Theorem breq2d 4100

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  breqtrd  4114  sbcbr1g  4145  pofun  4409  csbfv12g  5679  isorel  5948  isocnv  5951  isotr  5956  caovordig  6187  caovordg  6189  caovord  6193  xporderlem  6395  th3qlem2  6806  phplem3g  7041  supsnti  7203  inflbti  7222  difinfinf  7299  enqdc1  7581  ltanqg  7619  ltmnqg  7620  archnqq  7636  prarloclemarch2  7638  prloc  7710  addnqprllem  7746  addlocprlemgt  7753  appdivnq  7782  mulnqprl  7787  1idprl  7809  ltexprlemloc  7826  caucvgprlemcanl  7863  cauappcvgprlemm  7864  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlemlim  7880  cauappcvgpr  7881  archrecnq  7882  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemcl  7895  caucvgprlemladdrl  7897  caucvgpr  7901  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemnkeqj  7909  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  caucvgprprlem1  7928  caucvgprprlem2  7929  caucvgprpr  7931  ltposr  7982  ltasrg  7989  mulgt0sr  7997  mulextsr1lem  7999  mulextsr1  8000  prsrlt  8006  caucvgsrlemcl  8008  caucvgsrlemfv  8010  caucvgsrlembound  8013  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  caucvgsr  8021  map2psrprg  8024  pitonnlem2  8066  pitonn  8067  recidpipr  8075  axpre-ltadd  8105  axpre-mulgt0  8106  axpre-mulext  8107  axarch  8110  nntopi  8113  axcaucvglemval  8116  axcaucvglemcau  8117  axcaucvglemres  8118  axpre-suploclemres  8120  ltaddneg  8603  ltsubadd2  8612  lesubadd2  8614  ltaddsub  8615  leaddsub  8617  ltaddpos2  8632  posdif  8634  lesub1  8635  ltsub1  8637  ltnegcon1  8642  lenegcon1  8645  addge02  8652  leaddle0  8656  ltordlem  8661  possumd  8748  sublt0d  8749  apreap  8766  prodgt02  9032  prodge02  9034  ltmulgt12  9044  lemulge12  9046  ltdivmul  9055  ledivmul  9056  ltdivmul2  9057  lt2mul2div  9058  ledivmul2  9059  ltrec  9062  ltrec1  9067  ltdiv23  9071  lediv23  9072  nnge1  9165  halfpos  9374  lt2halves  9379  addltmul  9380  avglt2  9383  avgle2  9385  nnrecl  9399  zltlem1  9536  difgtsumgt  9548  nn0le2is012  9561  gtndiv  9574  qapne  9872  nnledivrp  10000  xltnegi  10069  xltadd1  10110  xsubge0  10115  xposdif  10116  xlesubadd  10117  xleaddadd  10121  divelunit  10236  eluzgtdifelfzo  10441  qtri3or  10499  exbtwnzlemstep  10506  exbtwnzlemshrink  10507  exbtwnzlemex  10508  exbtwnz  10509  rebtwn2zlemstep  10511  rebtwn2zlemshrink  10512  rebtwn2z  10513  flqlelt  10535  flqbi  10549  2tnp1ge0ge0  10560  q2submod  10646  frec2uzltd  10664  frec2uzlt2d  10665  frec2uzf1od  10667  monoord  10746  ser3mono  10748  ser3ge0  10797  expnbnd  10924  nn0ltexp2  10970  facwordi  11001  hashunlem  11066  zfz1isolemiso  11102  seq3coll  11105  swrdccat3blem  11319  caucvgrelemcau  11540  caucvgre  11541  cvg1nlemcau  11544  cvg1nlemres  11545  recvguniq  11555  resqrexlemover  11570  resqrexlemgt0  11580  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemsqa  11584  resqrexlemex  11585  maxleastlt  11775  minmax  11790  lemininf  11794  ltmininf  11795  xrmaxleastlt  11816  xrmaxltsup  11818  xrminmax  11825  xrmin1inf  11827  xrmin2inf  11828  xrltmininf  11830  xrlemininf  11831  climserle  11905  summodclem3  11940  summodclem2a  11941  summodc  11943  zsumdc  11944  fsum3  11947  fsum00  12022  fsumabs  12025  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  zproddc  12139  fprodseq  12143  fprodle  12200  sin01bnd  12317  cos01bnd  12318  summodnegmod  12382  modmulconst  12383  dvdsaddr  12397  dvdssub  12398  dvdssubr  12399  dvdslelemd  12403  dvdsfac  12420  dvdsmod  12422  oddp1even  12436  ltoddhalfle  12453  opoe  12455  omoe  12456  divalg2  12486  divalgmod  12487  ndvdssub  12490  ndvdsadd  12491  bitsfval  12502  bitsval  12503  bits0  12508  bitsp1  12511  bitsfzolem  12514  bitsfzo  12515  bitscmp  12518  bitsinv1lem  12521  bezoutlembi  12575  dvdssqim  12594  dvdsmulgcd  12595  dvdssq  12601  nn0seqcvgd  12612  coprmdvds  12663  coprmdvds2  12664  rpmul  12669  cncongr1  12674  divgcdodd  12714  isprm6  12718  prmdvdsexp  12719  prmdvdsexpr  12721  prmfac1  12723  oddpwdclemxy  12740  oddpwdclemodd  12743  sqpweven  12746  2sqpwodd  12747  sqne2sq  12748  hashdvds  12792  phiprmpw  12793  eulerthlemh  12802  prmdiv  12806  prmdiveq  12807  odzval  12813  odzcllem  12814  odzdvds  12817  pythagtriplem11  12846  pythagtriplem13  12848  pythagtrip  12855  pceulem  12866  pczndvds2  12890  pcdvdsb  12892  pc2dvds  12902  pcz  12904  pcprmpw2  12905  dvdsprmpweq  12907  dvdsprmpweqle  12909  difsqpwdvds  12910  pcmpt  12915  prmpwdvds  12927  pockthlem  12928  4sqlem11  12973  exmidunben  13046  nninfdclemlt  13071  mulgval  13708  dvdsrtr  14114  dvdsrmul1  14115  unitnegcl  14143  unitpropdg  14161  elrhmunit  14190  zndvds0  14663  znunit  14672  mplsubgfilemcl  14712  psmettri2  15051  ismet2  15077  xmettri2  15084  comet  15222  ivthinclemum  15358  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemdisj  15363  ivthinclemloc  15364  ivthinc  15366  ivthreinc  15368  limccl  15382  ellimc3apf  15383  sin0pilem2  15505  pilem3  15506  sincosq1sgn  15549  sincosq2sgn  15550  sincosq4sgn  15552  logltb  15597  logle1b  15615  loglt1b  15616  logbgt0b  15689  wilthlem1  15703  sgmval  15706  dvdsppwf1o  15712  perfect1  15721  lgslem1  15728  lgsval  15732  lgsdilem  15755  lgsne0  15766  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  lgseisenlem1  15798  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem2  15810  m1lgs  15813  2lgslem1a1  15814  2lgslem1a  15816  2lgsoddprmlem2  15834  2lgsoddprmlem3  15839  2sqlem4  15846  2sqlem8a  15850