Theorem breq1 4006

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
breq1	⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Proof of Theorem breq1

Step	Hyp	Ref	Expression
1		opeq1 3778	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	eleq1d 2246	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3		df-br 4004	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 4004	. 2 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148  ⟨cop 3595   class class class wbr 4003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004

This theorem is referenced by:  breq12  4008  breq1i  4010  breq1d  4013  nbrne2  4023  brab1  4050  pocl  4303  swopolem  4305  swopo  4306  issod  4319  sowlin  4320  sotritrieq  4325  frirrg  4350  wetriext  4576  vtoclr  4674  brcog  4794  brcogw  4796  opelcnvg  4807  dfdmf  4820  eldmg  4822  dfrnf  4868  dfres2  4959  imasng  4993  coi1  5144  dffun6f  5229  funmo  5231  fun11  5283  fveq2  5515  funfveu  5528  sefvex  5536  nfunsn  5549  fvmptss2  5591  f1ompt  5667  fmptco  5682  dff13  5768  foeqcnvco  5790  isorel  5808  isocnv  5811  isotr  5816  isoini  5818  isopolem  5822  isosolem  5824  f1oiso  5826  f1oiso2  5827  caovordig  6039  caovordg  6041  caovord3d  6044  caovord  6045  caovord3  6047  caofrss  6106  caoftrn  6107  poxp  6232  brtpos2  6251  rntpos  6257  tpostpos  6264  ertr  6549  ecopovsym  6630  ecopovtrn  6631  ecopovsymg  6633  ecopovtrng  6634  th3qlem2  6637  isfi  6760  en0  6794  en1  6798  en1bg  6799  endisj  6823  xpcomco  6825  dom0  6837  ssenen  6850  nneneq  6856  domfiexmid  6877  findcard  6887  findcard2  6888  findcard2s  6889  isinfinf  6896  tridc  6898  fimax2gtrilemstep  6899  fimax2gtri  6900  fiintim  6927  fisseneq  6930  en1eqsnbi  6947  isbth  6965  supmoti  6991  eqsupti  6994  supubti  6997  suplubti  6998  supsnti  7003  isotilem  7004  isoti  7005  supisolem  7006  supisoex  7007  infminti  7025  isnumi  7180  cardval3ex  7183  oncardval  7184  cardonle  7185  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidapne  7258  nqtri3or  7394  ltsonq  7396  ltanqg  7398  ltmnqg  7399  ltexnqq  7406  subhalfnqq  7412  ltbtwnnqq  7413  archnqq  7415  nqnq0pi  7436  prcdnql  7482  prcunqu  7483  prnmaxl  7486  genpcuu  7518  genprndl  7519  genprndu  7520  nqprm  7540  nqprrnd  7541  nqprdisj  7542  nqprloc  7543  nqpru  7550  addnqprlemrl  7555  addnqprlemfl  7557  addnqprlemfu  7558  prmuloc2  7565  mulnqprlemrl  7571  mulnqprlemfl  7573  mulnqprlemfu  7574  1idprl  7588  ltnqpr  7591  ltnqpri  7592  prplnqu  7618  recexprlemell  7620  recexprlemm  7622  recexprlemdisj  7628  recexprlemloc  7629  recexprlem1ssu  7632  recexprlemss1l  7633  aptiprlemu  7638  archpr  7641  cauappcvgprlemm  7643  cauappcvgprlemladdfl  7653  cauappcvgprlem2  7658  cauappcvgpr  7660  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemcl  7674  caucvgprlem2  7678  caucvgpr  7680  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnbj  7691  caucvgprprlemmu  7693  caucvgprprlemopu  7697  caucvgprprlemexbt  7704  caucvgprprlemaddq  7706  caucvgprprlem1  7707  caucvgprprlem2  7708  caucvgprpr  7710  suplocexprlemmu  7716  suplocexprlemloc  7719  suplocexpr  7723  lttrsr  7760  ltsosr  7762  1ne0sr  7764  ltasrg  7768  aptisr  7777  mulextsr1  7779  archsr  7780  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  caucvgsr  7800  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  axpre-ltwlin  7881  axpre-lttrn  7882  axpre-apti  7883  axpre-ltadd  7884  axpre-mulext  7886  axcaucvglemcau  7896  axcaucvglemres  7897  axcaucvg  7898  axpre-suploclemres  7899  axpre-suploc  7900  ltxrlt  8022  lttri3  8036  ltordlem  8438  lt0ne0d  8469  reapti  8535  apreim  8559  apsscn  8603  recexap  8609  lbreu  8901  lble  8903  suprleubex  8910  sup3exmid  8913  nnsub  8957  nominpos  9155  nn0n0n1ge2b  9331  zextle  9343  fzind  9367  btwnz  9371  uzval  9529  supinfneg  9594  infsupneg  9595  infregelbex  9597  ublbneg  9612  lbzbi  9615  qreccl  9641  xrltnsym  9792  xrlttr  9794  xrltso  9795  xrlttri3  9796  nltpnft  9813  npnflt  9814  xrrebnd  9818  xltnegi  9834  xnn0lenn0nn0  9864  xsubge0  9880  xlesubadd  9882  xleaddadd  9886  ixxval  9895  elixx1  9896  elioo2  9920  iccid  9924  fzval  10009  elfz1  10012  qtri3or  10242  exbtwnzlemstep  10247  exbtwnzlemshrink  10248  exbtwnzlemex  10249  exbtwnz  10250  rebtwn2zlemstep  10252  rebtwn2zlemshrink  10253  rebtwn2z  10254  qbtwnre  10256  qbtwnxr  10257  flval  10271  flqlelt  10275  flqbi  10289  flqeqceilz  10317  modqid2  10350  seq3f1olemqsum  10499  seq3f1oleml  10502  seq3f1o  10503  expcl2lemap  10531  expclzaplem  10543  expclzap  10544  expap0i  10551  nn0ltexp2  10688  hashinfuni  10756  hashennnuni  10758  hashunlem  10783  zfz1isolemiso  10818  zfz1isolem1  10819  zfz1iso  10820  absle  11097  maxleast  11221  rexanre  11228  rexico  11229  fimaxre2  11234  minmax  11237  xrmaxltsup  11265  xrminmax  11272  climshft  11311  reccn2ap  11320  summodclem3  11387  summodclem2a  11388  summodc  11390  zsumdc  11391  fsum3  11394  fsum3cvg3  11403  fsumcl2lem  11405  fsumadd  11413  sumsnf  11416  fsummulc2  11455  isumlessdc  11503  cvgratz  11539  mertenslemi1  11542  ntrivcvgap0  11556  prodmodclem3  11582  prodmodclem2a  11583  prodmodc  11585  zproddc  11586  fprodseq  11590  fprodntrivap  11591  fprodmul  11598  prodsnf  11599  absdvdsb  11815  zdvdsdc  11818  dvdsabseq  11852  dvdsdivcl  11855  dvdsext  11860  divalglemnn  11922  divalglemeunn  11925  divalglemeuneg  11927  divalgmod  11931  ndvdssub  11934  zsupcllemstep  11945  suprzubdc  11952  zsupssdc  11954  gcdsupex  11957  gcdsupcl  11958  gcddvds  11963  dvdslegcd  11964  bezoutlemmain  11998  bezoutlemex  12001  bezoutlemzz  12002  bezoutlemmo  12006  bezoutlemeu  12007  bezoutlemle  12008  bezoutlemsup  12009  dfgcd3  12010  dfgcd2  12014  gcdzeq  12022  dvdssq  12031  nnwodc  12036  uzwodc  12037  nnwofdc  12038  nn0seqcvgd  12040  algcvgblem  12048  lcmval  12062  lcmdvds  12078  lcmgcdeq  12082  coprmgcdb  12087  ncoprmgcdne1b  12088  coprmdvds1  12090  1nprm  12113  1idssfct  12114  isprm2lem  12115  isprm2  12116  dvdsprime  12121  nprm  12122  3prm  12127  dvdsprm  12136  exprmfct  12137  isprm5lem  12140  isprm5  12141  coprm  12143  sqrt2irr  12161  phisum  12239  odzval  12240  pythagtriplem4  12267  pc2dvds  12328  pcprmpw2  12331  pcprmpw  12332  dvdsprmpweqle  12335  oddprmdvds  12351  prmpwdvds  12352  pockthg  12354  1arith  12364  exmidunben  12426  nninfdclemcl  12448  nninfdclemp1  12450  nninfdc  12453  imasaddfnlemg  12734  ssblex  13901  comet  13969  bdmopn  13974  reopnap  14008  divcnap  14025  cdivcncfap  14057  cnopnap  14064  dedekindeulemuub  14065  dedekindeulemloc  14067  dedekindeulemlu  14069  dedekindeulemeu  14070  dedekindeu  14071  suplociccreex  14072  dedekindicclemuub  14074  dedekindicclemloc  14076  dedekindicclemlu  14078  dedekindicclemeu  14079  dedekindicclemicc  14080  dedekindicc  14081  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemloc  14089  ivthinc  14091  limcdifap  14101  limcimolemlt  14103  limccoap  14117  dvlemap  14119  dvidlemap  14130  dvcnp2cntop  14133  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  dvcjbr  14142  dvrecap  14147  dveflem  14157  logltb  14265  2irrexpqap  14366  lgsmod  14397  lgsne0  14409  2sqlem6  14437  2sqlem8  14440  2sqlem10  14442  pw1nct  14722  sbthom  14744  trilpo  14761  trirec0  14762  reap0  14776  dcapnconst  14778  neapmkv  14785  neap0mkv  14786  ltlenmkv  14787