Theorem breq2d 4001

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   class class class wbr 3989

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990

This theorem is referenced by:  breqtrd  4015  sbcbr1g  4045  pofun  4297  csbfv12g  5532  isorel  5787  isocnv  5790  isotr  5795  caovordig  6018  caovordg  6020  caovord  6024  xporderlem  6210  th3qlem2  6616  phplem3g  6834  supsnti  6982  inflbti  7001  difinfinf  7078  enqdc1  7324  ltanqg  7362  ltmnqg  7363  archnqq  7379  prarloclemarch2  7381  prloc  7453  addnqprllem  7489  addlocprlemgt  7496  appdivnq  7525  mulnqprl  7530  1idprl  7552  ltexprlemloc  7569  caucvgprlemcanl  7606  cauappcvgprlemm  7607  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlemlim  7623  cauappcvgpr  7624  archrecnq  7625  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemcl  7638  caucvgprlemladdrl  7640  caucvgpr  7644  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnkeqj  7652  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlemclphr  7667  caucvgprprlemexbt  7668  caucvgprprlem1  7671  caucvgprprlem2  7672  caucvgprpr  7674  ltposr  7725  ltasrg  7732  mulgt0sr  7740  mulextsr1lem  7742  mulextsr1  7743  prsrlt  7749  caucvgsrlemcl  7751  caucvgsrlemfv  7753  caucvgsrlembound  7756  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  caucvgsr  7764  map2psrprg  7767  pitonnlem2  7809  pitonn  7810  recidpipr  7818  axpre-ltadd  7848  axpre-mulgt0  7849  axpre-mulext  7850  axarch  7853  nntopi  7856  axcaucvglemval  7859  axcaucvglemcau  7860  axcaucvglemres  7861  axpre-suploclemres  7863  ltaddneg  8343  ltsubadd2  8352  lesubadd2  8354  ltaddsub  8355  leaddsub  8357  ltaddpos2  8372  posdif  8374  lesub1  8375  ltsub1  8377  ltnegcon1  8382  lenegcon1  8385  addge02  8392  leaddle0  8396  ltordlem  8401  possumd  8488  sublt0d  8489  apreap  8506  prodgt02  8769  prodge02  8771  ltmulgt12  8781  lemulge12  8783  ltdivmul  8792  ledivmul  8793  ltdivmul2  8794  lt2mul2div  8795  ledivmul2  8796  ltrec  8799  ltrec1  8804  ltdiv23  8808  lediv23  8809  nnge1  8901  halfpos  9109  lt2halves  9113  addltmul  9114  avglt2  9117  avgle2  9119  nnrecl  9133  zltlem1  9269  difgtsumgt  9281  nn0le2is012  9294  gtndiv  9307  qapne  9598  nnledivrp  9723  xltnegi  9792  xltadd1  9833  xsubge0  9838  xposdif  9839  xlesubadd  9840  xleaddadd  9844  divelunit  9959  eluzgtdifelfzo  10153  qtri3or  10199  exbtwnzlemstep  10204  exbtwnzlemshrink  10205  exbtwnzlemex  10206  exbtwnz  10207  rebtwn2zlemstep  10209  rebtwn2zlemshrink  10210  rebtwn2z  10211  flqlelt  10232  flqbi  10246  2tnp1ge0ge0  10257  q2submod  10341  frec2uzltd  10359  frec2uzlt2d  10360  frec2uzf1od  10362  monoord  10432  ser3mono  10434  ser3ge0  10473  expnbnd  10599  nn0ltexp2  10644  facwordi  10674  hashunlem  10739  zfz1isolemiso  10774  seq3coll  10777  caucvgrelemcau  10944  caucvgre  10945  cvg1nlemcau  10948  cvg1nlemres  10949  recvguniq  10959  resqrexlemover  10974  resqrexlemgt0  10984  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemsqa  10988  resqrexlemex  10989  maxleastlt  11179  minmax  11193  lemininf  11197  ltmininf  11198  xrmaxleastlt  11219  xrmaxltsup  11221  xrminmax  11228  xrmin1inf  11230  xrmin2inf  11231  xrltmininf  11233  xrlemininf  11234  climserle  11308  summodclem3  11343  summodclem2a  11344  summodc  11346  zsumdc  11347  fsum3  11350  fsum00  11425  fsumabs  11428  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  zproddc  11542  fprodseq  11546  fprodle  11603  sin01bnd  11720  cos01bnd  11721  summodnegmod  11784  modmulconst  11785  dvdsaddr  11799  dvdssub  11800  dvdssubr  11801  dvdslelemd  11803  dvdsfac  11820  dvdsmod  11822  oddp1even  11835  ltoddhalfle  11852  opoe  11854  omoe  11855  divalg2  11885  divalgmod  11886  ndvdssub  11889  ndvdsadd  11890  bezoutlembi  11960  dvdssqim  11979  dvdsmulgcd  11980  dvdssq  11986  nn0seqcvgd  11995  coprmdvds  12046  coprmdvds2  12047  rpmul  12052  cncongr1  12057  divgcdodd  12097  isprm6  12101  prmdvdsexp  12102  prmdvdsexpr  12104  prmfac1  12106  oddpwdclemxy  12123  oddpwdclemodd  12126  sqpweven  12129  2sqpwodd  12130  sqne2sq  12131  hashdvds  12175  phiprmpw  12176  eulerthlemh  12185  prmdiv  12189  prmdiveq  12190  odzval  12195  odzcllem  12196  odzdvds  12199  pythagtriplem11  12228  pythagtriplem13  12230  pythagtrip  12237  pceulem  12248  pczndvds2  12271  pcdvdsb  12273  pc2dvds  12283  pcz  12285  pcprmpw2  12286  dvdsprmpweq  12288  dvdsprmpweqle  12290  difsqpwdvds  12291  pcmpt  12295  prmpwdvds  12307  pockthlem  12308  exmidunben  12381  nninfdclemlt  12406  psmettri2  13122  ismet2  13148  xmettri2  13155  comet  13293  ivthinclemum  13407  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemdisj  13412  ivthinclemloc  13413  ivthinc  13415  limccl  13422  ellimc3apf  13423  sin0pilem2  13497  pilem3  13498  sincosq1sgn  13541  sincosq2sgn  13542  sincosq4sgn  13544  logltb  13589  logle1b  13607  loglt1b  13608  logbgt0b  13678  lgslem1  13695  lgsval  13699  lgsdilem  13722  lgsne0  13733  2sqlem4  13748  2sqlem8a  13752