Theorem breq2d 4121

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 4113	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   class class class wbr 4109

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110

This theorem is referenced by:  breqtrd  4135  sbcbr1g  4166  pofun  4433  csbfv12g  5710  isorel  5981  isocnv  5984  isotr  5989  caovordig  6220  caovordg  6222  caovord  6226  xporderlem  6427  th3qlem2  6872  phplem3g  7110  supsnti  7296  inflbti  7315  difinfinf  7392  enqdc1  7677  ltanqg  7715  ltmnqg  7716  archnqq  7732  prarloclemarch2  7734  prloc  7806  addnqprllem  7842  addlocprlemgt  7849  appdivnq  7878  mulnqprl  7883  1idprl  7905  ltexprlemloc  7922  caucvgprlemcanl  7959  cauappcvgprlemm  7960  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  cauappcvgprlemlim  7976  cauappcvgpr  7977  archrecnq  7978  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemcl  7991  caucvgprlemladdrl  7993  caucvgpr  7997  caucvgprprlemell  8000  caucvgprprlemelu  8001  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemnkeqj  8005  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemloc  8018  caucvgprprlemclphr  8020  caucvgprprlemexbt  8021  caucvgprprlem1  8024  caucvgprprlem2  8025  caucvgprpr  8027  ltposr  8078  ltasrg  8085  mulgt0sr  8093  mulextsr1lem  8095  mulextsr1  8096  prsrlt  8102  caucvgsrlemcl  8104  caucvgsrlemfv  8106  caucvgsrlembound  8109  caucvgsrlemgt1  8110  caucvgsrlemoffres  8115  caucvgsr  8117  map2psrprg  8120  pitonnlem2  8162  pitonn  8163  recidpipr  8171  axpre-ltadd  8201  axpre-mulgt0  8202  axpre-mulext  8203  axarch  8206  nntopi  8209  axcaucvglemval  8212  axcaucvglemcau  8213  axcaucvglemres  8214  axpre-suploclemres  8216  ltaddneg  8698  ltsubadd2  8707  lesubadd2  8709  ltaddsub  8710  leaddsub  8712  ltaddpos2  8727  posdif  8729  lesub1  8730  ltsub1  8732  ltnegcon1  8737  lenegcon1  8740  addge02  8747  leaddle0  8751  ltordlem  8756  possumd  8843  sublt0d  8844  apreap  8861  prodgt02  9127  prodge02  9129  ltmulgt12  9139  lemulge12  9141  ltdivmul  9150  ledivmul  9151  ltdivmul2  9152  lt2mul2div  9153  ledivmul2  9154  ltrec  9157  ltrec1  9162  ltdiv23  9166  lediv23  9167  nnge1  9260  halfpos  9469  lt2halves  9474  addltmul  9475  avglt2  9478  avgle2  9480  nnrecl  9494  zltlem1  9635  difgtsumgt  9647  nn0le2is012  9660  gtndiv  9673  qapne  9971  nnledivrp  10099  xltnegi  10168  xltadd1  10209  xsubge0  10214  xposdif  10215  xlesubadd  10216  xleaddadd  10220  divelunit  10335  eluzgtdifelfzo  10542  qtri3or  10600  exbtwnzlemstep  10607  exbtwnzlemshrink  10608  exbtwnzlemex  10609  exbtwnz  10610  rebtwn2zlemstep  10612  rebtwn2zlemshrink  10613  rebtwn2z  10614  flqlelt  10636  flqbi  10650  2tnp1ge0ge0  10661  q2submod  10747  frec2uzltd  10765  frec2uzlt2d  10766  frec2uzf1od  10768  monoord  10847  ser3mono  10849  ser3ge0  10898  expnbnd  11025  nn0ltexp2  11071  facwordi  11102  hashunlem  11168  ssenneg  11204  zfz1isolemiso  11211  seq3coll  11214  swrdccat3blem  11431  caucvgrelemcau  11665  caucvgre  11666  cvg1nlemcau  11669  cvg1nlemres  11670  recvguniq  11680  resqrexlemover  11695  resqrexlemgt0  11705  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemsqa  11709  resqrexlemex  11710  maxleastlt  11900  minmax  11915  lemininf  11919  ltmininf  11920  xrmaxleastlt  11941  xrmaxltsup  11943  xrminmax  11950  xrmin1inf  11952  xrmin2inf  11953  xrltmininf  11955  xrlemininf  11956  climserle  12030  summodclem3  12066  summodclem2a  12067  summodc  12069  zsumdc  12070  fsum3  12073  fsum00  12148  fsumabs  12151  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  zproddc  12265  fprodseq  12269  fprodle  12326  sin01bnd  12443  cos01bnd  12444  summodnegmod  12508  modmulconst  12509  dvdsaddr  12523  dvdssub  12524  dvdssubr  12525  dvdslelemd  12529  dvdsfac  12546  dvdsmod  12548  oddp1even  12562  ltoddhalfle  12579  opoe  12581  omoe  12582  divalg2  12612  divalgmod  12613  ndvdssub  12616  ndvdsadd  12617  bitsfval  12628  bitsval  12629  bits0  12634  bitsp1  12637  bitsfzolem  12640  bitsfzo  12641  bitscmp  12644  bitsinv1lem  12647  bezoutlembi  12701  dvdssqim  12720  dvdsmulgcd  12721  dvdssq  12727  nn0seqcvgd  12738  coprmdvds  12789  coprmdvds2  12790  rpmul  12795  cncongr1  12800  divgcdodd  12840  isprm6  12844  prmdvdsexp  12845  prmdvdsexpr  12847  prmfac1  12849  oddpwdclemxy  12866  oddpwdclemodd  12869  sqpweven  12872  2sqpwodd  12873  sqne2sq  12874  hashdvds  12918  phiprmpw  12919  eulerthlemh  12928  prmdiv  12932  prmdiveq  12933  odzval  12939  odzcllem  12940  odzdvds  12943  pythagtriplem11  12972  pythagtriplem13  12974  pythagtrip  12981  pceulem  12992  pczndvds2  13016  pcdvdsb  13018  pc2dvds  13028  pcz  13030  pcprmpw2  13031  dvdsprmpweq  13033  dvdsprmpweqle  13035  difsqpwdvds  13036  pcmpt  13041  prmpwdvds  13053  pockthlem  13054  4sqlem11  13099  exmidunben  13177  nninfdclemlt  13202  mulgval  13839  dvdsrtr  14246  dvdsrmul1  14247  unitnegcl  14275  unitpropdg  14293  elrhmunit  14322  zndvds0  14798  znunit  14807  mplsubgfilemcl  14854  psmettri2  15193  ismet2  15219  xmettri2  15226  comet  15364  ivthinclemum  15500  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemdisj  15505  ivthinclemloc  15506  ivthinc  15508  ivthreinc  15510  limccl  15524  ellimc3apf  15525  sin0pilem2  15647  pilem3  15648  sincosq1sgn  15691  sincosq2sgn  15692  sincosq4sgn  15694  logltb  15739  logle1b  15757  loglt1b  15758  logbgt0b  15831  wilthlem1  15848  sgmval  15851  dvdsppwf1o  15857  perfect1  15866  lgslem1  15873  lgsval  15877  lgsdilem  15900  lgsne0  15911  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  lgseisenlem1  15943  lgseisenlem2  15944  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem2  15955  m1lgs  15958  2lgslem1a1  15959  2lgslem1a  15961  2lgsoddprmlem2  15979  2lgsoddprmlem3  15984  2sqlem4  15991  2sqlem8a  15995  eupth2lem3lem3fi  16465  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  eupth2lem3lem7fi  16469  eupth2lemsfi  16473  eupth2fi  16474  konigsberglem4  16486