Theorem breq2 3933

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

Assertion

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

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 3706	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	eleq1d 2208	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3		df-br 3930	. 2 ⊢ (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4		df-br 3930	. 2 ⊢ (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 222	1 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   ∈ wcel 1480  ⟨cop 3530   class class class wbr 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930

This theorem is referenced by:  breq12  3934  breq2i  3937  breq2d  3941  nbrne1  3947  brralrspcev  3986  brimralrspcev  3987  pocl  4225  swopolem  4227  swopo  4228  sowlin  4242  sotricim  4245  sotritrieq  4247  seex  4257  frind  4274  wetriext  4491  vtoclr  4587  posng  4611  brcog  4706  brcogw  4708  opelcnvg  4719  dfdmf  4732  breldmg  4745  dfrnf  4780  dmcoss  4808  resieq  4829  dfres2  4871  elimag  4885  elreimasng  4905  elimasn  4906  intirr  4925  poirr2  4931  poltletr  4939  dffun6f  5136  dffun4f  5139  fun11  5190  brprcneu  5414  fv3  5444  tz6.12c  5451  relelfvdm  5453  funbrfv  5460  fnbrfvb  5462  funfvdm2f  5486  fndmdif  5525  dff3im  5565  fmptco  5586  foeqcnvco  5691  isorel  5709  isocnv  5712  isotr  5717  isopolem  5723  isosolem  5725  f1oiso  5727  f1oiso2  5728  caovordig  5936  caovordg  5938  caovord  5942  caofrss  6006  caoftrn  6007  poxp  6129  tposoprab  6177  ertr  6444  ecopovsym  6525  ecopovtrn  6526  ecopovsymg  6528  ecopovtrng  6529  th3qlem2  6532  domeng  6646  eqeng  6660  snfig  6708  nneneq  6751  nnfi  6766  ssfilem  6769  domfiexmid  6772  dif1enen  6774  diffitest  6781  findcard  6782  findcard2  6783  findcard2s  6784  diffisn  6787  tridc  6793  fimax2gtrilemstep  6794  inffiexmid  6800  unsnfi  6807  fiintim  6817  fisseneq  6820  isbth  6855  supmoti  6880  eqsupti  6883  supubti  6886  suplubti  6887  suplub2ti  6888  supmaxti  6891  supsnti  6892  isotilem  6893  isoti  6894  supisolem  6895  supisoex  6896  cardcl  7037  isnumi  7038  cardval3ex  7041  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  nqtri3or  7204  ltsonq  7206  ltanqg  7208  ltmnqg  7209  ltexnqq  7216  nsmallnqq  7220  subhalfnqq  7222  ltbtwnnqq  7223  prarloclemarch2  7227  nqnq0pi  7246  prcdnql  7292  prcunqu  7293  prnminu  7297  genpcdl  7327  genprndl  7329  genprndu  7330  genpdisj  7331  nqprm  7350  nqprrnd  7351  nqprdisj  7352  nqprloc  7353  nqprlu  7355  nqprl  7359  addnqprlemru  7366  addnqprlemfl  7367  addnqprlemfu  7368  mulnqprlemru  7382  mulnqprlemfl  7383  mulnqprlemfu  7384  1idpru  7399  ltnqpr  7401  ltnqpri  7402  prplnqu  7428  recexprlemelu  7431  recexprlemm  7432  recexprlemloc  7439  recexprlem1ssl  7441  recexprlemss1u  7444  cauappcvgprlemm  7453  cauappcvgprlemopu  7456  cauappcvgprlemupu  7457  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdfu  7462  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem2  7468  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemopu  7479  caucvgprlemupu  7480  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemcl  7484  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlem2  7488  caucvgprprlemelu  7494  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemnbj  7501  caucvgprprlemmu  7503  caucvgprprlemexbt  7514  caucvgprprlemaddq  7516  caucvgprprlem1  7517  caucvgprprlem2  7518  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  suplocexpr  7533  lttrsr  7570  ltsosr  7572  ltasrg  7578  recexgt0sr  7581  mulgt0sr  7586  aptisr  7587  mulextsr1  7589  srpospr  7591  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  caucvgsr  7610  map2psrprg  7613  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  axprecex  7688  axpre-ltwlin  7691  axpre-lttrn  7692  axpre-apti  7693  axpre-ltadd  7694  axpre-mulgt0  7695  axpre-mulext  7696  axcaucvglemcau  7706  axcaucvglemres  7707  axcaucvg  7708  axpre-suploclemres  7709  axpre-suploc  7710  ltxrlt  7830  lttri3  7844  ltne  7849  eqle  7855  ltordlem  8244  reapti  8341  apreim  8365  squeeze0  8662  lbreu  8703  lble  8705  suprleubex  8712  sup3exmid  8715  nnge1  8743  nn2ge  8753  nn1gt1  8754  nnsub  8759  nominpos  8957  nn0ge0  9002  elnnnn0b  9021  nn0ge2m1nn  9037  zdclt  9128  suprzclex  9149  peano2uz2  9158  peano5uzti  9159  dfuzi  9161  uzind  9162  uzind3  9164  eluz1  9330  uzind4  9383  indstr  9388  supinfneg  9390  infsupneg  9391  indstr2  9403  ublbneg  9405  elrp  9443  mnfltxr  9572  nn0pnfge0  9577  xrltnsym  9579  xrlttr  9581  xrltso  9582  xrlttri3  9583  xrltne  9596  ngtmnft  9600  nmnfgt  9601  xrrebnd  9602  z2ge  9609  xltnegi  9618  xltadd1  9659  xsubge0  9664  xleaddadd  9670  ixxval  9679  elixx1  9680  elioo2  9704  iccid  9708  iccsupr  9749  repos  9753  fzval  9792  elfz1  9795  fzm1  9880  exbtwnzlemstep  10025  exbtwnzlemex  10027  qbtwnre  10034  qbtwnxr  10035  flval  10045  apbtwnz  10047  modqid2  10124  modqmuladdnn0  10141  exp3val  10295  expge0  10329  expge1  10330  facdiv  10484  facwordi  10486  hashinfom  10524  hashennn  10526  hashunlem  10550  zfz1iso  10584  ovshftex  10591  shftfibg  10592  shftfib  10595  shftfn  10596  2shfti  10603  sqrt0rlem  10775  resqrexlemex  10797  rsqrmo  10799  resqrtcl  10801  rersqrtthlem  10802  sqrtsq  10816  cau3lem  10886  caubnd2  10889  maxleim  10977  maxabslemval  10980  maxleast  10985  maxleb  10988  fimaxre2  10998  minmax  11001  xrmaxleim  11013  xrmaxiflemval  11019  xrmaxaddlem  11029  xrminmax  11034  xrbdtri  11045  climi  11056  climeu  11065  climmo  11067  2clim  11070  addcn2  11079  mulcn2  11081  reccn2ap  11082  cn1lem  11083  summodc  11152  zsumdc  11153  fsum3  11156  cvgratz  11301  ntrivcvgap0  11318  prodmodc  11347  dvdsabsb  11512  0dvds  11513  alzdvds  11552  dvdsext  11553  fzo0dvdseq  11555  2tp1odd  11581  2teven  11584  divalglemnn  11615  divalglemeunn  11618  divalglemeuneg  11620  zsupcllemstep  11638  gcdval  11648  gcddvds  11652  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlemex  11689  bezoutlemeu  11695  bezoutlemsup  11697  dfgcd3  11698  bezout  11699  dvdsgcd  11700  dfgcd2  11702  dvdssq  11719  lcmval  11744  lcmcllem  11748  dvdslcm  11750  lcmledvds  11751  lcmgcdlem  11758  lcmdvds  11760  coprmgcdb  11769  coprmdvds2  11774  cncongr1  11784  cncongr2  11785  isprm  11790  dvdsnprmd  11806  dvdsprm  11817  exprmfct  11818  isprm6  11825  prmexpb  11829  prmfac1  11830  rpexp  11831  sqrt2irr  11840  oddpwdclemdc  11851  oddpwdc  11852  sqpweven  11853  2sqpwodd  11854  sqne2sq  11855  oddennn  11905  evenennn  11906  exmidunben  11939  comet  12668  metcnpi  12684  metcnpi2  12685  metcnpi3  12686  addcncntoplem  12720  cncfi  12734  elcncf1di  12735  mulcncflem  12759  dedekindeulemuub  12764  dedekindeulemloc  12766  dedekindeulemlu  12768  dedekindeulemeu  12769  dedekindeu  12770  suplociccreex  12771  suplociccex  12772  dedekindicclemuub  12773  dedekindicclemloc  12775  dedekindicclemlu  12777  dedekindicclemeu  12778  dedekindicclemicc  12779  dedekindicc  12780  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemloc  12788  ivthinc  12790  limcimo  12803  cnplimclemr  12807  limccnp2lem  12814  limccoap  12816  eldvap  12820  sbthom  13221  trilpo  13236