Theorem breq2d 4010

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   class class class wbr 3998

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999

This theorem is referenced by:  breqtrd  4024  sbcbr1g  4054  pofun  4306  csbfv12g  5543  isorel  5799  isocnv  5802  isotr  5807  caovordig  6030  caovordg  6032  caovord  6036  xporderlem  6222  th3qlem2  6628  phplem3g  6846  supsnti  6994  inflbti  7013  difinfinf  7090  enqdc1  7336  ltanqg  7374  ltmnqg  7375  archnqq  7391  prarloclemarch2  7393  prloc  7465  addnqprllem  7501  addlocprlemgt  7508  appdivnq  7537  mulnqprl  7542  1idprl  7564  ltexprlemloc  7581  caucvgprlemcanl  7618  cauappcvgprlemm  7619  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  cauappcvgprlem1  7633  cauappcvgprlemlim  7635  cauappcvgpr  7636  archrecnq  7637  caucvgprlemnkj  7640  caucvgprlemnbj  7641  caucvgprlemm  7642  caucvgprlemcl  7650  caucvgprlemladdrl  7652  caucvgpr  7656  caucvgprprlemell  7659  caucvgprprlemelu  7660  caucvgprprlemcbv  7661  caucvgprprlemval  7662  caucvgprprlemnkeqj  7664  caucvgprprlemml  7668  caucvgprprlemmu  7669  caucvgprprlemopl  7671  caucvgprprlemlol  7672  caucvgprprlemopu  7673  caucvgprprlemloc  7677  caucvgprprlemclphr  7679  caucvgprprlemexbt  7680  caucvgprprlem1  7683  caucvgprprlem2  7684  caucvgprpr  7686  ltposr  7737  ltasrg  7744  mulgt0sr  7752  mulextsr1lem  7754  mulextsr1  7755  prsrlt  7761  caucvgsrlemcl  7763  caucvgsrlemfv  7765  caucvgsrlembound  7768  caucvgsrlemgt1  7769  caucvgsrlemoffres  7774  caucvgsr  7776  map2psrprg  7779  pitonnlem2  7821  pitonn  7822  recidpipr  7830  axpre-ltadd  7860  axpre-mulgt0  7861  axpre-mulext  7862  axarch  7865  nntopi  7868  axcaucvglemval  7871  axcaucvglemcau  7872  axcaucvglemres  7873  axpre-suploclemres  7875  ltaddneg  8355  ltsubadd2  8364  lesubadd2  8366  ltaddsub  8367  leaddsub  8369  ltaddpos2  8384  posdif  8386  lesub1  8387  ltsub1  8389  ltnegcon1  8394  lenegcon1  8397  addge02  8404  leaddle0  8408  ltordlem  8413  possumd  8500  sublt0d  8501  apreap  8518  prodgt02  8781  prodge02  8783  ltmulgt12  8793  lemulge12  8795  ltdivmul  8804  ledivmul  8805  ltdivmul2  8806  lt2mul2div  8807  ledivmul2  8808  ltrec  8811  ltrec1  8816  ltdiv23  8820  lediv23  8821  nnge1  8913  halfpos  9121  lt2halves  9125  addltmul  9126  avglt2  9129  avgle2  9131  nnrecl  9145  zltlem1  9281  difgtsumgt  9293  nn0le2is012  9306  gtndiv  9319  qapne  9610  nnledivrp  9735  xltnegi  9804  xltadd1  9845  xsubge0  9850  xposdif  9851  xlesubadd  9852  xleaddadd  9856  divelunit  9971  eluzgtdifelfzo  10165  qtri3or  10211  exbtwnzlemstep  10216  exbtwnzlemshrink  10217  exbtwnzlemex  10218  exbtwnz  10219  rebtwn2zlemstep  10221  rebtwn2zlemshrink  10222  rebtwn2z  10223  flqlelt  10244  flqbi  10258  2tnp1ge0ge0  10269  q2submod  10353  frec2uzltd  10371  frec2uzlt2d  10372  frec2uzf1od  10374  monoord  10444  ser3mono  10446  ser3ge0  10485  expnbnd  10611  nn0ltexp2  10656  facwordi  10686  hashunlem  10750  zfz1isolemiso  10785  seq3coll  10788  caucvgrelemcau  10955  caucvgre  10956  cvg1nlemcau  10959  cvg1nlemres  10960  recvguniq  10970  resqrexlemover  10985  resqrexlemgt0  10995  resqrexlemoverl  10996  resqrexlemglsq  10997  resqrexlemsqa  10999  resqrexlemex  11000  maxleastlt  11190  minmax  11204  lemininf  11208  ltmininf  11209  xrmaxleastlt  11230  xrmaxltsup  11232  xrminmax  11239  xrmin1inf  11241  xrmin2inf  11242  xrltmininf  11244  xrlemininf  11245  climserle  11319  summodclem3  11354  summodclem2a  11355  summodc  11357  zsumdc  11358  fsum3  11361  fsum00  11436  fsumabs  11439  cvgratnnlemnexp  11498  cvgratnnlemmn  11499  zproddc  11553  fprodseq  11557  fprodle  11614  sin01bnd  11731  cos01bnd  11732  summodnegmod  11795  modmulconst  11796  dvdsaddr  11810  dvdssub  11811  dvdssubr  11812  dvdslelemd  11814  dvdsfac  11831  dvdsmod  11833  oddp1even  11846  ltoddhalfle  11863  opoe  11865  omoe  11866  divalg2  11896  divalgmod  11897  ndvdssub  11900  ndvdsadd  11901  bezoutlembi  11971  dvdssqim  11990  dvdsmulgcd  11991  dvdssq  11997  nn0seqcvgd  12006  coprmdvds  12057  coprmdvds2  12058  rpmul  12063  cncongr1  12068  divgcdodd  12108  isprm6  12112  prmdvdsexp  12113  prmdvdsexpr  12115  prmfac1  12117  oddpwdclemxy  12134  oddpwdclemodd  12137  sqpweven  12140  2sqpwodd  12141  sqne2sq  12142  hashdvds  12186  phiprmpw  12187  eulerthlemh  12196  prmdiv  12200  prmdiveq  12201  odzval  12206  odzcllem  12207  odzdvds  12210  pythagtriplem11  12239  pythagtriplem13  12241  pythagtrip  12248  pceulem  12259  pczndvds2  12282  pcdvdsb  12284  pc2dvds  12294  pcz  12296  pcprmpw2  12297  dvdsprmpweq  12299  dvdsprmpweqle  12301  difsqpwdvds  12302  pcmpt  12306  prmpwdvds  12318  pockthlem  12319  exmidunben  12392  nninfdclemlt  12417  mulgval  12845  psmettri2  13379  ismet2  13405  xmettri2  13412  comet  13550  ivthinclemum  13664  ivthinclemlopn  13665  ivthinclemlr  13666  ivthinclemuopn  13667  ivthinclemur  13668  ivthinclemdisj  13669  ivthinclemloc  13670  ivthinc  13672  limccl  13679  ellimc3apf  13680  sin0pilem2  13754  pilem3  13755  sincosq1sgn  13798  sincosq2sgn  13799  sincosq4sgn  13801  logltb  13846  logle1b  13864  loglt1b  13865  logbgt0b  13935  lgslem1  13952  lgsval  13956  lgsdilem  13979  lgsne0  13990  2sqlem4  14005  2sqlem8a  14009