Theorem breq1 2622

Description: Equality theorem for a binary relation.

Assertion

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

Proof of Theorem breq1

Step	Hyp	Ref	Expression
1		opeq1 2487	. . 3 |- (A = B -> <.A, C>. = <.B, C>.)
2	1	eleq1d 1540	. 2 |- (A = B -> (<.A, C>. e. R <-> <.B, C>. e. R))
3		df-br 2620	. 2 |- (ARC <-> <.A, C>. e. R)
4		df-br 2620	. 2 |- (BRC <-> <.B, C>. e. R)
5	2, 3, 4	3bitr4g 555	1 |- (A = B -> (ARC <-> BRC))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956   e. wcel 958  <.cop 2411   class class class wbr 2619

This theorem is referenced by:  breq12 2624  breq1i 2626  breq1d 2629  brab1 2660  pocl 2844  solin 2857  so 2864  dffr2 2919  frirr 2924  dfwe2 2935  wereu 2945  vtoclr 3211  vtoclrbr 3212  vtoclibr 3213  ididg 3278  opelco 3288  opelcog 3290  opelcnvg 3296  eldm 3307  breldmg 3316  imasng 3424  asymref2 3440  coi1 3510  dffunmof 3530  fun11 3562  fneu 3592  fv2 3720  tz6.12-2 3739  ndmfv 3745  funbrfv 3750  fnbrfvb 3753  dff2 3817  f1fv 3874  isorel 3894  isocnv 3896  isotr 3897  isotrALT 3898  isomin 3899  isoini 3900  isowe 3903  f1oiso 3904  f1oweALT 3906  caoprord 4056  caoprord3 4058  ertr 4274  erref 4275  erth 4282  ecopoprsym 4310  ecopoprtrn 4311  th3qlem2 4315  isfi 4382  ensymg 4411  en0 4423  en1 4426  endisj 4437  xpdom2 4442  sbth 4457  pwen 4503  ssenen 4504  nneneq 4512  php 4513  pssnn 4534  unifiOLD 4557  fiint 4559  fiintOLD 4560  abfii3OLD 4563  abfii4OLD 4564  fodomfiOLD 4566  iunfiOLD 4569  supmo 4576  supub 4580  suplub 4581  supmaxlem 4588  suppr 4590  supsnALT 4592  unbnnt 4639  kardex 4725  karden 4726  hta 4728  aceq3lem 4732  numth2 4785  numthcor 4786  zorn2lem2 4789  zorn2lem3 4790  zorn2lem7 4794  zorn2 4796  brdom7disj 4804  brdom6disj 4805  uniimadom 4810  oncardval 4819  oncardid 4821  cardonle 4822  cardid 4828  oncard 4829  cardne 4830  iscard2 4854  ondomon 4856  ondomcard 4857  alephon 4865  alephsuc 4866  alephval2 4902  ltpiord 5015  ltsopq 5075  ltapq 5076  ltmpq 5077  ltexpq 5080  ltbtwnpq 5084  prcdpq 5097  prnmax 5099  genpnmax 5110  1pr 5117  1idpr 5133  prlem934 5139  reclem2pr 5157  reclem3pr 5158  reclem4pr 5159  recexpr 5160  supexpr 5163  ltsosr 5203  1ne0sr 5205  ltasr 5209  suppsr 5222  suppsr2 5223  supsrlem6 5230  supre 5260  ltsor 5261  pre-axltadd 5289  lelttrt 5523  xrltnsymt 5550  xrlttrit 5552  xrlttrt 5553  xrlelttrt 5562  nltpnftt 5566  ltadd1t 5623  leadd1t 5625  ltsubaddt 5627  lesubaddt 5629  lt2addt 5643  le2addt 5644  ltnegt 5655  lenegt 5657  ltmul1t 5830  ltdiv1t 5849  ltdiv1tOLD 5850  ltmuldivt 5863  ltmuldivtOLD 5864  ltrec 5879  lt2msq 5881  ltrect 5884  lerect 5885  lt2msqt 5886  le2msqt 5903  posex 5908  xrmaxltt 5913  maxlet 5918  maxltt 5922  nnleltp1t 5954  nnsubt 5957  nominpos 6043  lbreu 6045  lble 6047  lbinfm 6048  sup2 6051  infm3 6054  infmsup 6068  nnunb 6070  arch 6071  xrinfmexpnf 6075  xrsupsslem 6076  xrinfmsslem 6077  xrub 6080  supxr 6081  supxrre 6083  supxrunb1 6089  supxrunb2 6090  nn0ltp1let 6127  nn0subt 6161  zltp1let 6181  zextlet 6189  peano5uzt 6204  uzwo4OLD 6210  uzwo5OLD 6211  btwnz 6215  uzwo3lem2 6217  uzwo3 6218  zmax 6220  rebtwnz 6222  flvalt 6225  flleltt 6228  flval2t 6238  flval3t 6239  flbit 6240  quoremOLD 6252  qbtwnre 6278  qbtwnxr 6279  ser1add2 6338  ser1add 6339  ioovalt 6366  iocvalt 6375  icovalt 6376  iccvalt 6377  elioo1t 6378  elioo2t 6379  elioc1t 6381  elico1t 6382  elicc1t 6383  icoun 6413  snunioolem 6414  snunioo 6415  uzvalt 6419  uzwo 6455  uzwoOLD 6456  nnwof 6459  uzinfm 6462  fzvalt 6469  elfz1t 6470  fsequb2 6524  sqlecant 6641  sqrlem6 6678  sqrlem12 6684  sqrlem18 6690  sqrlem20 6692  sqrlet 6713  sqr2irrlem2 6725  sqr2irrlem3 6726  abslt 6875  absle 6876  absltt 6880  abslet 6881  seq1ublem 6911  seq1ub 6912  cau3i 6914  cau3ir 6915  cau5i 6917  cvg1 6921  cvg3 6923  cvganz 6924  faclbnd4lem1 6948  bcvalt 6958  bcpasc2t 6968  bccl2t 6971  dffsum 6998  fsumsplit 7020  clm3 7079  clm4 7080  climfnn 7092  climconst 7094  climuni 7099  climshft 7104  climshft2 7106  climaddlem3 7116  climmullem8 7127  climsup 7155  caucvglem1 7157  caucvglem2 7158  caucvglem5 7161  caucvg3t 7168  serzf0 7169  ser1f0 7170  ser1clim0 7173  cvgcmpub 7185  cvgcmp3cet 7190  expcnvlem1 7227  expcnvlem5 7231  expcnvlem6 7232  efaddlem25 7362  eflegeot 7416  efm1legeot 7418  reefiso 7428  acdc3 7487  acdc2 7490  acdc5 7493  acdc 7495  unbenlem 7504  ruclem4 7513  ruclem33 7542  ruclem36 7545  infpss 7574  unctb 7577  infmap2lem1 7579  subbasOLD 7644  subbas2OLD 7645  fctopOLD 7650  qdensere 7751  ssblex 7856  tgioolem 7914  lmconst 7934  lmnn 7935  cmscvg 7947  lmfex 7959  metelcls 7965  metcn4i 7972  xplm 7975  xpcn 7976  iscms2lem4 7992  iscms2lem5 7993  bcthlem15 8013  nmoubi 8435  minveclem10 8554  spwmo 8656  spwpr2 8658  spwpr3OLD 8662  spwpr4OLD 8663  spwpr4aOLD 8664  pilem2 8672  pilem3 8673  logltbt 8776  chlim 9104  hlim0 9105  hlimcau 9107  hlimuni 9109  chcompl 9115  hsn0elch 9120  projlem8 9193  projlem13 9198  projlem28 9213  cmbr3t 9551  cmcmt 9557  cmcm3t 9558  lecmt 9560  nmopubt 9832  nmfnleubt 9849  nmopunt 9939  cnlnadjlem7 10006  bra11 10041  pjnmop 10075  stle0 10166  stles 10168  stm1 10170  csmdsym 10261  cvmdt 10263  atcveq0 10275  atcv1t 10307  atordt 10315  atcvat2t 10316  irredt 10322  mdsymt 10339  mddmdin0 10358  cdj1 10360  infi1OLD 10448  fineOLD 10450  abfiOLD 10452  ficliOLD 10473  top1 10547  top2ind 10548  top2usne 10549  fipfil2OLD 10565  filint2OLD 10575  infiOLD 10579  cnfilcaOLD 10584  rcfpfillem2OLD 10588  rcfpfillem3OLD 10590  rcfpfillem4OLD 10592  rcfpfillem5OLD 10594  rcfpfillem6OLD 10596

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620

Copyright terms: Public domain