Theorem breq1 2065

Description: Equality theorem for binary relation.

Assertion

Ref	Expression
breq1	|- (A = B -> (ARC <-> BRC))

Proof of Theorem breq1

Step	Hyp	Ref	Expression
1		opeq1 1876	. . 3 |- (A = B -> <.A, C>. = <.B, C>.)
2	1	eleq1d 1155	. 2 |- (A = B -> (<.A, C>. e. R <-> <.B, C>. e. R))
3		df-br 2063	. 2 |- (ARC <-> <.A, C>. e. R)
4		df-br 2063	. 2 |- (BRC <-> <.B, C>. e. R)
5	2, 3, 4	3bitr4g 428	1 |- (A = B -> (ARC <-> BRC))

Syntax hints:   -> wi 2   <-> wb 127   = wceq 1091   e. wcel 1092  <.cop 1810   class class class wbr 2054

This theorem is referenced by:  breq12 2067  breq1i 2068  breq1d 2071  brab1 2096  pocl 2132  solin 2145  so 2152  supmo 2156  supub 2160  suplub 2161  supsn 2168  dffr2 2171  frirr 2176  dfwe2 2187  wereu 2197  vtoclr 2449  vtoclrbr 2450  vtoclibr 2451  opelco 2509  opelcog 2511  opelcnvg 2517  eldm 2527  coi1 2665  dffunmof 2678  fneu 2728  fv2 2828  tz6.12-2 2845  ndmfv 2848  funbrfv 2852  fnfvbr 2855  f1fv 2916  isorel 2932  isocnv 2934  isotr 2935  isotrALT 2936  isomin 2937  isoini 2938  isowe 2941  f1oiso 2942  f1oweOLD 2944  caoprord 3070  caoprord3 3072  ertr 3211  erref 3212  erth 3219  ecopoprsym 3246  ecopoprtrn 3247  th3qlem2 3251  ensymg 3316  en0 3328  en1 3331  endisj 3341  sbth 3359  ssenen 3399  nneneq 3408  php 3409  pssnn 3428  fiint 3445  kardex 3550  karden 3551  aceq3lem 3555  numth2 3600  numthcor 3601  zornlem2 3604  zornlem3 3605  zornlem7 3609  zorn 3611  hta 3619  oncardval 3626  oncardid 3628  cardonle 3629  cardid 3635  oncard 3636  cardne 3637  iscard2 3660  ondomon 3662  ondomcard 3663  alephon 3671  alephsuc 3672  ltpiord 3809  ltsopq 3869  ltapq 3870  ltmpq 3871  ltexpq 3874  ltbtwnpq 3878  prcdpq 3891  prnmax 3893  genpnmax 3904  1pr 3911  1idpr 3927  prlem934 3933  reclem2pr 3951  reclem3pr 3952  reclem4pr 3953  recexpr 3954  suppr 3957  ltsosr 3997  1ne0sr 3999  ltasr 4003  suppsr 4016  suppsr2 4017  supsrlem6 4024  supre 4054  ltsor 4055  axltadd 4085  lelttrt 4289  letrit 4347  ltadd1t 4348  leadd1t 4350  ltsubaddt 4353  lesubaddt 4355  lt2addt 4361  posdift 4365  ltnegt 4366  lenegt 4368  ltdivt 4404  ltmuldivt 4406  ltrec 4410  lt2sq 4414  ltrect 4417  lerect 4418  le2sqt 4420  posex 4422  nnleltp1t 4448  nnsubt 4451  nominpos 4509  sup2 4510  nnunb 4520  arch 4521  nn0ltp1let 4556  nn0subt 4587  zltp1let 4597  uzwo 4605  uzwo2 4606  nnwoOLD 4608  nnwof 4609  btwnz 4613  uzwo3lem2 4615  uzwo3 4616  zmax 4618  rebtwnz 4620  flvalt 4623  flleltt 4625  qbtwnre 4650  lt2sqet 4706  sqrlem6 4736  sqrlem12 4742  sqrlem18 4748  sqrlem20 4750  sqr2irrlem2 4778  sqr2irrlem3 4779  abslt 4855  absle 4856  absltt 4857  clim0 4882  climuni 4884  ruclem4 4888  ruclem33 4917  ruclem36 4920  infmap2lem1 4951  chlim 5139  hlim0 5140  hlimcau 5142  hlimuni 5144  chcompl 5150  hsn0elch 5155  projlem8 5200  projlem13 5205  projlem28 5220  stle0 5680  stles 5682  stm1 5684  atcveq0 5746  atcv1 5768  atcvat2t 5773

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