Theorem breq2 2066

Description: Equality theorem for binary relation.

Assertion

Ref	Expression
breq2	⊢ (A = B → (CRA ↔ CRB))

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 1877	. . 3 ⊢ (A = B → ⟨C, A⟩ = ⟨C, B⟩)
2	1	eleq1d 1155	. 2 ⊢ (A = B → (⟨C, A⟩ ∈ R ↔ ⟨C, B⟩ ∈ R))
3		df-br 2063	. 2 ⊢ (CRA ↔ ⟨C, A⟩ ∈ R)
4		df-br 2063	. 2 ⊢ (CRB ↔ ⟨C, B⟩ ∈ R)
5	2, 3, 4	3bitr4g 428	1 ⊢ (A = B → (CRA ↔ CRB))

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091   ∈ wcel 1092  ⟨cop 1810   class class class wbr 2054

This theorem is referenced by:  breq12 2067  breq2i 2069  breq2d 2072  pocl 2132  solin 2145  sotric 2148  sotrieq 2149  so 2152  supmo 2156  supub 2160  suplub 2161  supsn 2168  dffr2 2171  frirr 2176  fr2nr 2177  fr3nr 2178  dfwe2 2187  wereu 2197  vtoclr 2449  vtoclrbr 2450  vtoclibr 2451  opelco 2509  opelcog 2511  opelcnvg 2517  resieq 2581  elima 2606  eliniseg 2618  dffun3 2675  dffunmof 2678  fv3 2839  tz6.12c 2846  tz6.12i 2847  funbrfv 2852  fnfvbr 2855  isorel 2932  isocnv 2934  isotr 2935  isotrALT 2936  isowe 2941  f1oiso 2942  f1oweOLD 2944  caoprord 3070  ertr 3211  erref 3212  elec 3216  ecopoprsym 3246  ecopoprtrn 3247  th3qlem2 3251  domeng 3285  eqeng 3296  ensymg 3316  snfi 3337  sbth 3359  nneneq 3408  php2 3410  php3 3411  onfin 3415  ominf 3423  omsdomnn 3424  pssnn 3428  ssnn 3429  ssfi 3430  unfi 3441  fiint 3445  aceq3lem 3555  numth2 3600  zornlem2 3604  zornlem7 3609  zorn 3611  fodomg 3614  hta 3619  oncardval 3626  cardval 3633  carden 3638  unxpdom 3650  sucxpdom 3652  cardlim 3657  cardmin 3666  alephnbtwn 3674  alephordlem1 3677  cardaleph 3690  ltpiord 3809  indpi 3828  ltsopq 3869  ltapq 3870  ltmpq 3871  ltexpq 3874  nsmallpq 3877  ltbtwnpq 3878  ltrpq 3879  prcdpq 3891  genpcd 3903  genpnmax 3904  prlem934b 3932  ltaddpr2 3935  ltexprlem4 3939  reclem3pr 3952  suppr 3957  ltsosr 3997  ltasr 4003  recexsrlem 4006  mulgt0sr 4008  map2psrpr 4014  suppsrlem 4015  suppsr 4016  suppsr2 4017  suppsr3 4018  supsrlem5 4023  supsrlem6 4024  supre 4054  ltsor 4055  axltadd 4085  axmulgt0 4086  ltletrt 4290  letrt 4291  gt0ne0t 4346  letrit 4347  ltadd1t 4348  leadd1t 4350  ltsubaddt 4353  lesubaddt 4355  lt2addt 4361  addge0t 4362  posdift 4365  ltnegt 4366  lenegt 4368  lesub0t 4374  mulge0t 4375  elimgt0 4381  elimge0 4382  recgt0t 4401  divgt0t 4402  divge0t 4403  ltdivt 4404  ltmuldivt 4406  ltrec 4410  ltdiv23 4413  ltrect 4417  lerect 4418  ltdiv23t 4419  le2sqt 4420  posex 4422  nn2get 4438  nnge1t 4439  nnleltp1t 4448  nnsub 4450  nnsubt 4451  halfpost 4508  nominpos 4509  sup2 4510  nnunb 4520  lt0nnn0 4549  nn0ltp1let 4556  elnnz1 4581  nn0subt 4587  zltp1let 4597  peano2uz 4602  uzind 4603  uzind2 4604  uzwo 4605  uzwo2 4606  nnwof 4609  uzwo3lem2 4615  uzwo3 4616  zmin 4617  zmax 4618  zbtwnre 4619  rebtwnz 4620  flvalt 4623  qbtwnre 4650  om2uzuz 4653  om2uzran 4655  uzrdgini 4658  sqe11t 4705  lt2sqet 4706  sqrval 4729  sqr0 4730  sqrlem4 4734  sqrlem6 4736  sqrlem12 4742  sqrlem13 4743  sqrlem20 4750  sqrlem21 4751  sqrlem22 4752  sqrlem24 4754  sqrgt0i 4755  sqrlem26 4756  sqrclt 4767  sqrgt0t 4768  sqrge0t 4769  sqr00t 4770  sqsqrt 4776  sqr2irrlem1 4777  sqr2irrlem2 4778  sqr2irr 4782  absltt 4857  absidt 4862  abs3lemt 4865  climunii 4883  climuni 4884  ruclem4 4888  ruclem33 4917  ruclem35 4919  ruclem36 4920  infxpidmlem2 4934  infxpidmlem3 4935  infxpidmlem8 4940  infmap2 4953  norm3lemt 5097  chlim 5139  hlimcaui 5141  hlimcau 5142  hlimunii 5143  hlimuni 5144  hlimreu 5145  hlimeu 5146  occllem6 5185  occllem8 5187  projlem1 5193  projlem7 5199  projlem8 5200  projlem15 5207  projlem20 5212  projlem29 5221  pjssge0 5573  pjnormss 5638  stge1 5679  strlem5 5696  elat 5738

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-un 1490  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063

metamath.org