Theorem breq1 3788

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 3570	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	eleq1d 2147	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3		df-br 3786	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 3786	. 2 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 221	1 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1284   ∈ wcel 1433  ⟨cop 3401   class class class wbr 3785

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-br 3786

This theorem is referenced by:  breq12  3790  breq1i  3792  breq1d  3795  nbrne2  3803  brab1  3830  pocl  4058  swopolem  4060  swopo  4061  issod  4074  sowlin  4075  sotritrieq  4080  frirrg  4105  wetriext  4319  vtoclr  4406  brcog  4520  brcogw  4522  opelcnvg  4533  dfdmf  4546  eldmg  4548  dfrnf  4593  dfres2  4678  imasng  4710  coi1  4856  dffun6f  4935  funmo  4937  fun11  4986  fveq2  5198  funfveu  5208  sefvex  5216  nfunsn  5228  fvmptss2  5268  f1ompt  5341  fmptco  5351  dff13  5428  foeqcnvco  5450  isorel  5468  isocnv  5471  isotr  5476  isoini  5477  isopolem  5481  isosolem  5483  f1oiso  5485  f1oiso2  5486  caovordig  5686  caovordg  5688  caovord3d  5691  caovord  5692  caovord3  5694  caofrss  5755  caoftrn  5756  poxp  5873  brtpos2  5889  rntpos  5895  tpostpos  5902  ertr  6144  ecopovsym  6225  ecopovtrn  6226  ecopovsymg  6228  ecopovtrng  6229  th3qlem2  6232  isfi  6264  en0  6298  en1  6302  en1bg  6303  endisj  6321  xpcomco  6323  nneneq  6343  domfiexmid  6363  findcard  6372  findcard2  6373  findcard2s  6374  supmoti  6406  eqsupti  6409  supubti  6412  suplubti  6413  supsnti  6418  isotilem  6419  isoti  6420  supisolem  6421  supisoex  6422  infminti  6440  isnumi  6451  cardval3ex  6454  oncardval  6455  cardonle  6456  nqtri3or  6586  ltsonq  6588  ltanqg  6590  ltmnqg  6591  ltexnqq  6598  subhalfnqq  6604  ltbtwnnqq  6605  archnqq  6607  nqnq0pi  6628  prcdnql  6674  prcunqu  6675  prnmaxl  6678  genpcuu  6710  genprndl  6711  genprndu  6712  nqprm  6732  nqprrnd  6733  nqprdisj  6734  nqprloc  6735  nqpru  6742  addnqprlemrl  6747  addnqprlemfl  6749  addnqprlemfu  6750  prmuloc2  6757  mulnqprlemrl  6763  mulnqprlemfl  6765  mulnqprlemfu  6766  1idprl  6780  ltnqpr  6783  ltnqpri  6784  prplnqu  6810  recexprlemell  6812  recexprlemm  6814  recexprlemdisj  6820  recexprlemloc  6821  recexprlem1ssu  6824  recexprlemss1l  6825  aptiprlemu  6830  archpr  6833  cauappcvgprlemm  6835  cauappcvgprlemladdfl  6845  cauappcvgprlem2  6850  cauappcvgpr  6852  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemcl  6866  caucvgprlem2  6870  caucvgpr  6872  caucvgprprlemelu  6876  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemnbj  6883  caucvgprprlemmu  6885  caucvgprprlemopu  6889  caucvgprprlemexbt  6896  caucvgprprlemaddq  6898  caucvgprprlem1  6899  caucvgprprlem2  6900  caucvgprpr  6902  lttrsr  6939  ltsosr  6941  1ne0sr  6943  ltasrg  6947  aptisr  6955  mulextsr1  6957  archsr  6958  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  caucvgsr  6978  axpre-ltwlin  7049  axpre-lttrn  7050  axpre-apti  7051  axpre-ltadd  7052  axpre-mulext  7054  axcaucvglemcau  7064  axcaucvglemres  7065  axcaucvg  7066  ltxrlt  7178  lttri3  7191  lt0ne0d  7614  reapti  7679  apreim  7703  recexap  7743  lbreu  8023  lble  8025  suprleubex  8032  nnsub  8077  nominpos  8268  nn0n0n1ge2b  8427  zextle  8438  fzind  8462  btwnz  8466  uzval  8621  supinfneg  8683  infsupneg  8684  ublbneg  8698  lbzbi  8701  qreccl  8727  xrltnsym  8868  xrlttr  8870  xrltso  8871  xrlttri3  8872  nltpnft  8884  xrrebnd  8886  xltnegi  8902  ixxval  8919  elixx1  8920  elioo2  8944  iccid  8948  fzval  9031  elfz1  9034  qtri3or  9252  qbtwnzlemstep  9257  qbtwnzlemshrink  9258  qbtwnzlemex  9259  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2zlemshrink  9262  rebtwn2z  9263  qbtwnre  9265  qbtwnxr  9266  flval  9276  flqlelt  9278  flqbi  9292  flqeqceilz  9320  modqid2  9353  expcl2lemap  9488  expclzaplem  9500  expclzap  9501  expap0i  9508  absle  9975  maxleast  10099  rexanre  10106  rexico  10107  fimaxre2  10109  minmax  10112  climshft  10143  absdvdsb  10213  zdvdsdc  10216  dvdsabseq  10247  dvdsdivcl  10250  dvdsext  10255  divalglemnn  10318  divalglemeunn  10321  divalglemeuneg  10323  divalgmod  10327  ndvdssub  10330  zsupcllemstep  10341  gcdsupex  10349  gcdsupcl  10350  gcddvds  10355  dvdslegcd  10356  bezoutlemmain  10387  bezoutlemex  10390  bezoutlemzz  10391  bezoutlemmo  10395  bezoutlemeu  10396  bezoutlemle  10397  bezoutlemsup  10398  dfgcd3  10399  dfgcd2  10403  gcdzeq  10411  dvdssq  10420  nn0seqcvgd  10423  algcvgblem  10431  lcmval  10445  lcmdvds  10461  lcmgcdeq  10465  coprmgcdb  10470  ncoprmgcdne1b  10471  coprmdvds1  10473  1nprm  10496  1idssfct  10497  isprm2lem  10498  isprm2  10499  dvdsprime  10504  nprm  10505  3prm  10510  dvdsprm  10518  exprmfct  10519  coprm  10523  sqrt2irr  10541