Theorem breq1 3870

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1296   ∈ wcel 1445  ⟨cop 3469   class class class wbr 3867

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-br 3868

This theorem is referenced by:  breq12  3872  breq1i  3874  breq1d  3877  nbrne2  3885  brab1  3912  pocl  4154  swopolem  4156  swopo  4157  issod  4170  sowlin  4171  sotritrieq  4176  frirrg  4201  wetriext  4420  vtoclr  4515  brcog  4634  brcogw  4636  opelcnvg  4647  dfdmf  4660  eldmg  4662  dfrnf  4708  dfres2  4797  imasng  4830  coi1  4980  dffun6f  5062  funmo  5064  fun11  5115  fveq2  5340  funfveu  5353  sefvex  5361  nfunsn  5373  fvmptss2  5414  f1ompt  5489  fmptco  5503  dff13  5585  foeqcnvco  5607  isorel  5625  isocnv  5628  isotr  5633  isoini  5635  isopolem  5639  isosolem  5641  f1oiso  5643  f1oiso2  5644  caovordig  5848  caovordg  5850  caovord3d  5853  caovord  5854  caovord3  5856  caofrss  5917  caoftrn  5918  poxp  6035  brtpos2  6054  rntpos  6060  tpostpos  6067  ertr  6347  ecopovsym  6428  ecopovtrn  6429  ecopovsymg  6431  ecopovtrng  6432  th3qlem2  6435  isfi  6558  en0  6592  en1  6596  en1bg  6597  endisj  6620  xpcomco  6622  dom0  6634  ssenen  6647  nneneq  6653  domfiexmid  6674  findcard  6684  findcard2  6685  findcard2s  6686  isinfinf  6693  tridc  6695  fimax2gtrilemstep  6696  fimax2gtri  6697  fiintim  6719  fisseneq  6722  en1eqsnbi  6738  isbth  6756  supmoti  6768  eqsupti  6771  supubti  6774  suplubti  6775  supsnti  6780  isotilem  6781  isoti  6782  supisolem  6783  supisoex  6784  infminti  6802  isnumi  6907  cardval3ex  6910  oncardval  6911  cardonle  6912  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  nqtri3or  7052  ltsonq  7054  ltanqg  7056  ltmnqg  7057  ltexnqq  7064  subhalfnqq  7070  ltbtwnnqq  7071  archnqq  7073  nqnq0pi  7094  prcdnql  7140  prcunqu  7141  prnmaxl  7144  genpcuu  7176  genprndl  7177  genprndu  7178  nqprm  7198  nqprrnd  7199  nqprdisj  7200  nqprloc  7201  nqpru  7208  addnqprlemrl  7213  addnqprlemfl  7215  addnqprlemfu  7216  prmuloc2  7223  mulnqprlemrl  7229  mulnqprlemfl  7231  mulnqprlemfu  7232  1idprl  7246  ltnqpr  7249  ltnqpri  7250  prplnqu  7276  recexprlemell  7278  recexprlemm  7280  recexprlemdisj  7286  recexprlemloc  7287  recexprlem1ssu  7290  recexprlemss1l  7291  aptiprlemu  7296  archpr  7299  cauappcvgprlemm  7301  cauappcvgprlemladdfl  7311  cauappcvgprlem2  7316  cauappcvgpr  7318  caucvgprlemnkj  7322  caucvgprlemnbj  7323  caucvgprlemcl  7332  caucvgprlem2  7336  caucvgpr  7338  caucvgprprlemelu  7342  caucvgprprlemcbv  7343  caucvgprprlemval  7344  caucvgprprlemnbj  7349  caucvgprprlemmu  7351  caucvgprprlemopu  7355  caucvgprprlemexbt  7362  caucvgprprlemaddq  7364  caucvgprprlem1  7365  caucvgprprlem2  7366  caucvgprpr  7368  lttrsr  7405  ltsosr  7407  1ne0sr  7409  ltasrg  7413  aptisr  7421  mulextsr1  7423  archsr  7424  caucvgsrlemgt1  7437  caucvgsrlemoffres  7442  caucvgsr  7444  axpre-ltwlin  7515  axpre-lttrn  7516  axpre-apti  7517  axpre-ltadd  7518  axpre-mulext  7520  axcaucvglemcau  7530  axcaucvglemres  7531  axcaucvg  7532  ltxrlt  7649  lttri3  7662  ltordlem  8057  lt0ne0d  8088  reapti  8153  apreim  8177  recexap  8219  lbreu  8503  lble  8505  suprleubex  8512  sup3exmid  8515  nnsub  8559  nominpos  8751  nn0n0n1ge2b  8924  zextle  8936  fzind  8960  btwnz  8964  uzval  9120  supinfneg  9182  infsupneg  9183  ublbneg  9197  lbzbi  9200  qreccl  9226  xrltnsym  9362  xrlttr  9364  xrltso  9365  xrlttri3  9366  nltpnft  9380  npnflt  9381  xrrebnd  9385  xltnegi  9401  xnn0lenn0nn0  9431  xsubge0  9447  xlesubadd  9449  xleaddadd  9453  ixxval  9462  elixx1  9463  elioo2  9487  iccid  9491  fzval  9575  elfz1  9578  qtri3or  9803  exbtwnzlemstep  9808  exbtwnzlemshrink  9809  exbtwnzlemex  9810  exbtwnz  9811  rebtwn2zlemstep  9813  rebtwn2zlemshrink  9814  rebtwn2z  9815  qbtwnre  9817  qbtwnxr  9818  flval  9828  flqlelt  9832  flqbi  9846  flqeqceilz  9874  modqid2  9907  seq3f1olemqsum  10050  seq3f1oleml  10053  seq3f1o  10054  expcl2lemap  10082  expclzaplem  10094  expclzap  10095  expap0i  10102  hashinfuni  10300  hashennnuni  10302  hashunlem  10327  zfz1isolemiso  10359  zfz1isolem1  10360  zfz1iso  10361  absle  10637  maxleast  10761  rexanre  10768  rexico  10769  fimaxre2  10773  minmax  10776  xrmaxltsup  10801  xrminmax  10808  climshft  10847  reccn2ap  10856  summodclem3  10923  summodclem2a  10924  summodc  10926  zsumdc  10927  fsum3  10930  fsum3cvg3  10939  fsumcl2lem  10941  fsumadd  10949  sumsnf  10952  fsummulc2  10991  isumlessdc  11039  cvgratz  11075  mertenslemi1  11078  absdvdsb  11241  zdvdsdc  11244  dvdsabseq  11275  dvdsdivcl  11278  dvdsext  11283  divalglemnn  11345  divalglemeunn  11348  divalglemeuneg  11350  divalgmod  11354  ndvdssub  11357  zsupcllemstep  11368  gcdsupex  11376  gcdsupcl  11377  gcddvds  11382  dvdslegcd  11383  bezoutlemmain  11414  bezoutlemex  11417  bezoutlemzz  11418  bezoutlemmo  11422  bezoutlemeu  11423  bezoutlemle  11424  bezoutlemsup  11425  dfgcd3  11426  dfgcd2  11430  gcdzeq  11438  dvdssq  11447  nn0seqcvgd  11450  algcvgblem  11458  lcmval  11472  lcmdvds  11488  lcmgcdeq  11492  coprmgcdb  11497  ncoprmgcdne1b  11498  coprmdvds1  11500  1nprm  11523  1idssfct  11524  isprm2lem  11525  isprm2  11526  dvdsprime  11531  nprm  11532  3prm  11537  dvdsprm  11545  exprmfct  11546  coprm  11550  sqrt2irr  11568  ssblex  12217  comet  12285  bdmopn  12290  cdivcncfap  12350