Theorem breq2d 4030

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   class class class wbr 4018

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-br 4019

This theorem is referenced by:  breqtrd  4044  sbcbr1g  4074  pofun  4327  csbfv12g  5568  isorel  5826  isocnv  5829  isotr  5834  caovordig  6058  caovordg  6060  caovord  6064  xporderlem  6251  th3qlem2  6659  phplem3g  6879  supsnti  7029  inflbti  7048  difinfinf  7125  enqdc1  7386  ltanqg  7424  ltmnqg  7425  archnqq  7441  prarloclemarch2  7443  prloc  7515  addnqprllem  7551  addlocprlemgt  7558  appdivnq  7587  mulnqprl  7592  1idprl  7614  ltexprlemloc  7631  caucvgprlemcanl  7668  cauappcvgprlemm  7669  cauappcvgprlemladdru  7680  cauappcvgprlemladdrl  7681  cauappcvgprlem1  7683  cauappcvgprlemlim  7685  cauappcvgpr  7686  archrecnq  7687  caucvgprlemnkj  7690  caucvgprlemnbj  7691  caucvgprlemm  7692  caucvgprlemcl  7700  caucvgprlemladdrl  7702  caucvgpr  7706  caucvgprprlemell  7709  caucvgprprlemelu  7710  caucvgprprlemcbv  7711  caucvgprprlemval  7712  caucvgprprlemnkeqj  7714  caucvgprprlemml  7718  caucvgprprlemmu  7719  caucvgprprlemopl  7721  caucvgprprlemlol  7722  caucvgprprlemopu  7723  caucvgprprlemloc  7727  caucvgprprlemclphr  7729  caucvgprprlemexbt  7730  caucvgprprlem1  7733  caucvgprprlem2  7734  caucvgprpr  7736  ltposr  7787  ltasrg  7794  mulgt0sr  7802  mulextsr1lem  7804  mulextsr1  7805  prsrlt  7811  caucvgsrlemcl  7813  caucvgsrlemfv  7815  caucvgsrlembound  7818  caucvgsrlemgt1  7819  caucvgsrlemoffres  7824  caucvgsr  7826  map2psrprg  7829  pitonnlem2  7871  pitonn  7872  recidpipr  7880  axpre-ltadd  7910  axpre-mulgt0  7911  axpre-mulext  7912  axarch  7915  nntopi  7918  axcaucvglemval  7921  axcaucvglemcau  7922  axcaucvglemres  7923  axpre-suploclemres  7925  ltaddneg  8406  ltsubadd2  8415  lesubadd2  8417  ltaddsub  8418  leaddsub  8420  ltaddpos2  8435  posdif  8437  lesub1  8438  ltsub1  8440  ltnegcon1  8445  lenegcon1  8448  addge02  8455  leaddle0  8459  ltordlem  8464  possumd  8551  sublt0d  8552  apreap  8569  prodgt02  8835  prodge02  8837  ltmulgt12  8847  lemulge12  8849  ltdivmul  8858  ledivmul  8859  ltdivmul2  8860  lt2mul2div  8861  ledivmul2  8862  ltrec  8865  ltrec1  8870  ltdiv23  8874  lediv23  8875  nnge1  8967  halfpos  9175  lt2halves  9179  addltmul  9180  avglt2  9183  avgle2  9185  nnrecl  9199  zltlem1  9335  difgtsumgt  9347  nn0le2is012  9360  gtndiv  9373  qapne  9664  nnledivrp  9791  xltnegi  9860  xltadd1  9901  xsubge0  9906  xposdif  9907  xlesubadd  9908  xleaddadd  9912  divelunit  10027  eluzgtdifelfzo  10222  qtri3or  10268  exbtwnzlemstep  10273  exbtwnzlemshrink  10274  exbtwnzlemex  10275  exbtwnz  10276  rebtwn2zlemstep  10278  rebtwn2zlemshrink  10279  rebtwn2z  10280  flqlelt  10302  flqbi  10316  2tnp1ge0ge0  10327  q2submod  10411  frec2uzltd  10429  frec2uzlt2d  10430  frec2uzf1od  10432  monoord  10502  ser3mono  10504  ser3ge0  10543  expnbnd  10670  nn0ltexp2  10716  facwordi  10747  hashunlem  10811  zfz1isolemiso  10846  seq3coll  10849  caucvgrelemcau  11016  caucvgre  11017  cvg1nlemcau  11020  cvg1nlemres  11021  recvguniq  11031  resqrexlemover  11046  resqrexlemgt0  11056  resqrexlemoverl  11057  resqrexlemglsq  11058  resqrexlemsqa  11060  resqrexlemex  11061  maxleastlt  11251  minmax  11265  lemininf  11269  ltmininf  11270  xrmaxleastlt  11291  xrmaxltsup  11293  xrminmax  11300  xrmin1inf  11302  xrmin2inf  11303  xrltmininf  11305  xrlemininf  11306  climserle  11380  summodclem3  11415  summodclem2a  11416  summodc  11418  zsumdc  11419  fsum3  11422  fsum00  11497  fsumabs  11500  cvgratnnlemnexp  11559  cvgratnnlemmn  11560  zproddc  11614  fprodseq  11618  fprodle  11675  sin01bnd  11792  cos01bnd  11793  summodnegmod  11856  modmulconst  11857  dvdsaddr  11871  dvdssub  11872  dvdssubr  11873  dvdslelemd  11876  dvdsfac  11893  dvdsmod  11895  oddp1even  11908  ltoddhalfle  11925  opoe  11927  omoe  11928  divalg2  11958  divalgmod  11959  ndvdssub  11962  ndvdsadd  11963  bezoutlembi  12033  dvdssqim  12052  dvdsmulgcd  12053  dvdssq  12059  nn0seqcvgd  12068  coprmdvds  12119  coprmdvds2  12120  rpmul  12125  cncongr1  12130  divgcdodd  12170  isprm6  12174  prmdvdsexp  12175  prmdvdsexpr  12177  prmfac1  12179  oddpwdclemxy  12196  oddpwdclemodd  12199  sqpweven  12202  2sqpwodd  12203  sqne2sq  12204  hashdvds  12248  phiprmpw  12249  eulerthlemh  12258  prmdiv  12262  prmdiveq  12263  odzval  12268  odzcllem  12269  odzdvds  12272  pythagtriplem11  12301  pythagtriplem13  12303  pythagtrip  12310  pceulem  12321  pczndvds2  12345  pcdvdsb  12347  pc2dvds  12357  pcz  12359  pcprmpw2  12360  dvdsprmpweq  12362  dvdsprmpweqle  12364  difsqpwdvds  12365  pcmpt  12370  prmpwdvds  12382  pockthlem  12383  4sqlem11  12428  exmidunben  12472  nninfdclemlt  12497  mulgval  13057  dvdsrtr  13444  dvdsrmul1  13445  unitnegcl  13473  unitpropdg  13491  elrhmunit  13520  psmettri2  14265  ismet2  14291  xmettri2  14298  comet  14436  ivthinclemum  14550  ivthinclemlopn  14551  ivthinclemlr  14552  ivthinclemuopn  14553  ivthinclemur  14554  ivthinclemdisj  14555  ivthinclemloc  14556  ivthinc  14558  limccl  14565  ellimc3apf  14566  sin0pilem2  14640  pilem3  14641  sincosq1sgn  14684  sincosq2sgn  14685  sincosq4sgn  14687  logltb  14732  logle1b  14750  loglt1b  14751  logbgt0b  14821  lgslem1  14838  lgsval  14842  lgsdilem  14865  lgsne0  14876  lgseisenlem1  14887  lgseisenlem2  14888  m1lgs  14889  2lgsoddprmlem2  14891  2lgsoddprmlem3  14896  2sqlem4  14902  2sqlem8a  14906