Theorem breq2d 4100

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
breq2d	⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Proof of Theorem breq2d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq2 4092	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  breqtrd  4114  sbcbr1g  4145  pofun  4409  csbfv12g  5679  isorel  5949  isocnv  5952  isotr  5957  caovordig  6188  caovordg  6190  caovord  6194  xporderlem  6396  th3qlem2  6807  phplem3g  7042  supsnti  7204  inflbti  7223  difinfinf  7300  enqdc1  7582  ltanqg  7620  ltmnqg  7621  archnqq  7637  prarloclemarch2  7639  prloc  7711  addnqprllem  7747  addlocprlemgt  7754  appdivnq  7783  mulnqprl  7788  1idprl  7810  ltexprlemloc  7827  caucvgprlemcanl  7864  cauappcvgprlemm  7865  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  cauappcvgpr  7882  archrecnq  7883  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemcl  7896  caucvgprlemladdrl  7898  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgprpr  7932  ltposr  7983  ltasrg  7990  mulgt0sr  7998  mulextsr1lem  8000  mulextsr1  8001  prsrlt  8007  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsrlembound  8014  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  caucvgsr  8022  map2psrprg  8025  pitonnlem2  8067  pitonn  8068  recidpipr  8076  axpre-ltadd  8106  axpre-mulgt0  8107  axpre-mulext  8108  axarch  8111  nntopi  8114  axcaucvglemval  8117  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  ltaddneg  8604  ltsubadd2  8613  lesubadd2  8615  ltaddsub  8616  leaddsub  8618  ltaddpos2  8633  posdif  8635  lesub1  8636  ltsub1  8638  ltnegcon1  8643  lenegcon1  8646  addge02  8653  leaddle0  8657  ltordlem  8662  possumd  8749  sublt0d  8750  apreap  8767  prodgt02  9033  prodge02  9035  ltmulgt12  9045  lemulge12  9047  ltdivmul  9056  ledivmul  9057  ltdivmul2  9058  lt2mul2div  9059  ledivmul2  9060  ltrec  9063  ltrec1  9068  ltdiv23  9072  lediv23  9073  nnge1  9166  halfpos  9375  lt2halves  9380  addltmul  9381  avglt2  9384  avgle2  9386  nnrecl  9400  zltlem1  9537  difgtsumgt  9549  nn0le2is012  9562  gtndiv  9575  qapne  9873  nnledivrp  10001  xltnegi  10070  xltadd1  10111  xsubge0  10116  xposdif  10117  xlesubadd  10118  xleaddadd  10122  divelunit  10237  eluzgtdifelfzo  10443  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemshrink  10509  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2zlemshrink  10514  rebtwn2z  10515  flqlelt  10537  flqbi  10551  2tnp1ge0ge0  10562  q2submod  10648  frec2uzltd  10666  frec2uzlt2d  10667  frec2uzf1od  10669  monoord  10748  ser3mono  10750  ser3ge0  10799  expnbnd  10926  nn0ltexp2  10972  facwordi  11003  hashunlem  11068  zfz1isolemiso  11104  seq3coll  11107  swrdccat3blem  11324  caucvgrelemcau  11558  caucvgre  11559  cvg1nlemcau  11562  cvg1nlemres  11563  recvguniq  11573  resqrexlemover  11588  resqrexlemgt0  11598  resqrexlemoverl  11599  resqrexlemglsq  11600  resqrexlemsqa  11602  resqrexlemex  11603  maxleastlt  11793  minmax  11808  lemininf  11812  ltmininf  11813  xrmaxleastlt  11834  xrmaxltsup  11836  xrminmax  11843  xrmin1inf  11845  xrmin2inf  11846  xrltmininf  11848  xrlemininf  11849  climserle  11923  summodclem3  11959  summodclem2a  11960  summodc  11962  zsumdc  11963  fsum3  11966  fsum00  12041  fsumabs  12044  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  zproddc  12158  fprodseq  12162  fprodle  12219  sin01bnd  12336  cos01bnd  12337  summodnegmod  12401  modmulconst  12402  dvdsaddr  12416  dvdssub  12417  dvdssubr  12418  dvdslelemd  12422  dvdsfac  12439  dvdsmod  12441  oddp1even  12455  ltoddhalfle  12472  opoe  12474  omoe  12475  divalg2  12505  divalgmod  12506  ndvdssub  12509  ndvdsadd  12510  bitsfval  12521  bitsval  12522  bits0  12527  bitsp1  12530  bitsfzolem  12533  bitsfzo  12534  bitscmp  12537  bitsinv1lem  12540  bezoutlembi  12594  dvdssqim  12613  dvdsmulgcd  12614  dvdssq  12620  nn0seqcvgd  12631  coprmdvds  12682  coprmdvds2  12683  rpmul  12688  cncongr1  12693  divgcdodd  12733  isprm6  12737  prmdvdsexp  12738  prmdvdsexpr  12740  prmfac1  12742  oddpwdclemxy  12759  oddpwdclemodd  12762  sqpweven  12765  2sqpwodd  12766  sqne2sq  12767  hashdvds  12811  phiprmpw  12812  eulerthlemh  12821  prmdiv  12825  prmdiveq  12826  odzval  12832  odzcllem  12833  odzdvds  12836  pythagtriplem11  12865  pythagtriplem13  12867  pythagtrip  12874  pceulem  12885  pczndvds2  12909  pcdvdsb  12911  pc2dvds  12921  pcz  12923  pcprmpw2  12924  dvdsprmpweq  12926  dvdsprmpweqle  12928  difsqpwdvds  12929  pcmpt  12934  prmpwdvds  12946  pockthlem  12947  4sqlem11  12992  exmidunben  13065  nninfdclemlt  13090  mulgval  13727  dvdsrtr  14134  dvdsrmul1  14135  unitnegcl  14163  unitpropdg  14181  elrhmunit  14210  zndvds0  14683  znunit  14692  mplsubgfilemcl  14732  psmettri2  15071  ismet2  15097  xmettri2  15104  comet  15242  ivthinclemum  15378  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemdisj  15383  ivthinclemloc  15384  ivthinc  15386  ivthreinc  15388  limccl  15402  ellimc3apf  15403  sin0pilem2  15525  pilem3  15526  sincosq1sgn  15569  sincosq2sgn  15570  sincosq4sgn  15572  logltb  15617  logle1b  15635  loglt1b  15636  logbgt0b  15709  wilthlem1  15723  sgmval  15726  dvdsppwf1o  15732  perfect1  15741  lgslem1  15748  lgsval  15752  lgsdilem  15775  lgsne0  15786  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  lgseisenlem1  15818  lgseisenlem2  15819  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem2  15830  m1lgs  15833  2lgslem1a1  15834  2lgslem1a  15836  2lgsoddprmlem2  15854  2lgsoddprmlem3  15859  2sqlem4  15866  2sqlem8a  15870  eupth2lem3lem3fi  16340  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343  eupth2lem3lem7fi  16344  eupth2lemsfi  16348  eupth2fi  16349  konigsberglem4  16361