Theorem breq2d 4015

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

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004

This theorem is referenced by:  breqtrd  4029  sbcbr1g  4059  pofun  4312  csbfv12g  5551  isorel  5808  isocnv  5811  isotr  5816  caovordig  6039  caovordg  6041  caovord  6045  xporderlem  6231  th3qlem2  6637  phplem3g  6855  supsnti  7003  inflbti  7022  difinfinf  7099  enqdc1  7360  ltanqg  7398  ltmnqg  7399  archnqq  7415  prarloclemarch2  7417  prloc  7489  addnqprllem  7525  addlocprlemgt  7532  appdivnq  7561  mulnqprl  7566  1idprl  7588  ltexprlemloc  7605  caucvgprlemcanl  7642  cauappcvgprlemm  7643  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem1  7657  cauappcvgprlemlim  7659  cauappcvgpr  7660  archrecnq  7661  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemcl  7674  caucvgprlemladdrl  7676  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem1  7707  caucvgprprlem2  7708  caucvgprpr  7710  ltposr  7761  ltasrg  7768  mulgt0sr  7776  mulextsr1lem  7778  mulextsr1  7779  prsrlt  7785  caucvgsrlemcl  7787  caucvgsrlemfv  7789  caucvgsrlembound  7792  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  caucvgsr  7800  map2psrprg  7803  pitonnlem2  7845  pitonn  7846  recidpipr  7854  axpre-ltadd  7884  axpre-mulgt0  7885  axpre-mulext  7886  axarch  7889  nntopi  7892  axcaucvglemval  7895  axcaucvglemcau  7896  axcaucvglemres  7897  axpre-suploclemres  7899  ltaddneg  8380  ltsubadd2  8389  lesubadd2  8391  ltaddsub  8392  leaddsub  8394  ltaddpos2  8409  posdif  8411  lesub1  8412  ltsub1  8414  ltnegcon1  8419  lenegcon1  8422  addge02  8429  leaddle0  8433  ltordlem  8438  possumd  8525  sublt0d  8526  apreap  8543  prodgt02  8809  prodge02  8811  ltmulgt12  8821  lemulge12  8823  ltdivmul  8832  ledivmul  8833  ltdivmul2  8834  lt2mul2div  8835  ledivmul2  8836  ltrec  8839  ltrec1  8844  ltdiv23  8848  lediv23  8849  nnge1  8941  halfpos  9149  lt2halves  9153  addltmul  9154  avglt2  9157  avgle2  9159  nnrecl  9173  zltlem1  9309  difgtsumgt  9321  nn0le2is012  9334  gtndiv  9347  qapne  9638  nnledivrp  9765  xltnegi  9834  xltadd1  9875  xsubge0  9880  xposdif  9881  xlesubadd  9882  xleaddadd  9886  divelunit  10001  eluzgtdifelfzo  10196  qtri3or  10242  exbtwnzlemstep  10247  exbtwnzlemshrink  10248  exbtwnzlemex  10249  exbtwnz  10250  rebtwn2zlemstep  10252  rebtwn2zlemshrink  10253  rebtwn2z  10254  flqlelt  10275  flqbi  10289  2tnp1ge0ge0  10300  q2submod  10384  frec2uzltd  10402  frec2uzlt2d  10403  frec2uzf1od  10405  monoord  10475  ser3mono  10477  ser3ge0  10516  expnbnd  10643  nn0ltexp2  10688  facwordi  10719  hashunlem  10783  zfz1isolemiso  10818  seq3coll  10821  caucvgrelemcau  10988  caucvgre  10989  cvg1nlemcau  10992  cvg1nlemres  10993  recvguniq  11003  resqrexlemover  11018  resqrexlemgt0  11028  resqrexlemoverl  11029  resqrexlemglsq  11030  resqrexlemsqa  11032  resqrexlemex  11033  maxleastlt  11223  minmax  11237  lemininf  11241  ltmininf  11242  xrmaxleastlt  11263  xrmaxltsup  11265  xrminmax  11272  xrmin1inf  11274  xrmin2inf  11275  xrltmininf  11277  xrlemininf  11278  climserle  11352  summodclem3  11387  summodclem2a  11388  summodc  11390  zsumdc  11391  fsum3  11394  fsum00  11469  fsumabs  11472  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  zproddc  11586  fprodseq  11590  fprodle  11647  sin01bnd  11764  cos01bnd  11765  summodnegmod  11828  modmulconst  11829  dvdsaddr  11843  dvdssub  11844  dvdssubr  11845  dvdslelemd  11848  dvdsfac  11865  dvdsmod  11867  oddp1even  11880  ltoddhalfle  11897  opoe  11899  omoe  11900  divalg2  11930  divalgmod  11931  ndvdssub  11934  ndvdsadd  11935  bezoutlembi  12005  dvdssqim  12024  dvdsmulgcd  12025  dvdssq  12031  nn0seqcvgd  12040  coprmdvds  12091  coprmdvds2  12092  rpmul  12097  cncongr1  12102  divgcdodd  12142  isprm6  12146  prmdvdsexp  12147  prmdvdsexpr  12149  prmfac1  12151  oddpwdclemxy  12168  oddpwdclemodd  12171  sqpweven  12174  2sqpwodd  12175  sqne2sq  12176  hashdvds  12220  phiprmpw  12221  eulerthlemh  12230  prmdiv  12234  prmdiveq  12235  odzval  12240  odzcllem  12241  odzdvds  12244  pythagtriplem11  12273  pythagtriplem13  12275  pythagtrip  12282  pceulem  12293  pczndvds2  12316  pcdvdsb  12318  pc2dvds  12328  pcz  12330  pcprmpw2  12331  dvdsprmpweq  12333  dvdsprmpweqle  12335  difsqpwdvds  12336  pcmpt  12340  prmpwdvds  12352  pockthlem  12353  exmidunben  12426  nninfdclemlt  12451  mulgval  12985  dvdsrtr  13268  dvdsrmul1  13269  unitnegcl  13297  unitpropdg  13315  psmettri2  13798  ismet2  13824  xmettri2  13831  comet  13969  ivthinclemum  14083  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemdisj  14088  ivthinclemloc  14089  ivthinc  14091  limccl  14098  ellimc3apf  14099  sin0pilem2  14173  pilem3  14174  sincosq1sgn  14217  sincosq2sgn  14218  sincosq4sgn  14220  logltb  14265  logle1b  14283  loglt1b  14284  logbgt0b  14354  lgslem1  14371  lgsval  14375  lgsdilem  14398  lgsne0  14409  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2lgsoddprmlem2  14424  2lgsoddprmlem3  14429  2sqlem4  14435  2sqlem8a  14439