Theorem breq2d 4056

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   class class class wbr 4044

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4045

This theorem is referenced by:  breqtrd  4070  sbcbr1g  4100  pofun  4359  csbfv12g  5614  isorel  5877  isocnv  5880  isotr  5885  caovordig  6112  caovordg  6114  caovord  6118  xporderlem  6317  th3qlem2  6725  phplem3g  6953  supsnti  7107  inflbti  7126  difinfinf  7203  enqdc1  7475  ltanqg  7513  ltmnqg  7514  archnqq  7530  prarloclemarch2  7532  prloc  7604  addnqprllem  7640  addlocprlemgt  7647  appdivnq  7676  mulnqprl  7681  1idprl  7703  ltexprlemloc  7720  caucvgprlemcanl  7757  cauappcvgprlemm  7758  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlemlim  7774  cauappcvgpr  7775  archrecnq  7776  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemcl  7789  caucvgprlemladdrl  7791  caucvgpr  7795  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnkeqj  7803  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  caucvgprprlem1  7822  caucvgprprlem2  7823  caucvgprpr  7825  ltposr  7876  ltasrg  7883  mulgt0sr  7891  mulextsr1lem  7893  mulextsr1  7894  prsrlt  7900  caucvgsrlemcl  7902  caucvgsrlemfv  7904  caucvgsrlembound  7907  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  caucvgsr  7915  map2psrprg  7918  pitonnlem2  7960  pitonn  7961  recidpipr  7969  axpre-ltadd  7999  axpre-mulgt0  8000  axpre-mulext  8001  axarch  8004  nntopi  8007  axcaucvglemval  8010  axcaucvglemcau  8011  axcaucvglemres  8012  axpre-suploclemres  8014  ltaddneg  8497  ltsubadd2  8506  lesubadd2  8508  ltaddsub  8509  leaddsub  8511  ltaddpos2  8526  posdif  8528  lesub1  8529  ltsub1  8531  ltnegcon1  8536  lenegcon1  8539  addge02  8546  leaddle0  8550  ltordlem  8555  possumd  8642  sublt0d  8643  apreap  8660  prodgt02  8926  prodge02  8928  ltmulgt12  8938  lemulge12  8940  ltdivmul  8949  ledivmul  8950  ltdivmul2  8951  lt2mul2div  8952  ledivmul2  8953  ltrec  8956  ltrec1  8961  ltdiv23  8965  lediv23  8966  nnge1  9059  halfpos  9268  lt2halves  9273  addltmul  9274  avglt2  9277  avgle2  9279  nnrecl  9293  zltlem1  9430  difgtsumgt  9442  nn0le2is012  9455  gtndiv  9468  qapne  9760  nnledivrp  9888  xltnegi  9957  xltadd1  9998  xsubge0  10003  xposdif  10004  xlesubadd  10005  xleaddadd  10009  divelunit  10124  eluzgtdifelfzo  10326  qtri3or  10383  exbtwnzlemstep  10390  exbtwnzlemshrink  10391  exbtwnzlemex  10392  exbtwnz  10393  rebtwn2zlemstep  10395  rebtwn2zlemshrink  10396  rebtwn2z  10397  flqlelt  10419  flqbi  10433  2tnp1ge0ge0  10444  q2submod  10530  frec2uzltd  10548  frec2uzlt2d  10549  frec2uzf1od  10551  monoord  10630  ser3mono  10632  ser3ge0  10681  expnbnd  10808  nn0ltexp2  10854  facwordi  10885  hashunlem  10949  zfz1isolemiso  10984  seq3coll  10987  caucvgrelemcau  11291  caucvgre  11292  cvg1nlemcau  11295  cvg1nlemres  11296  recvguniq  11306  resqrexlemover  11321  resqrexlemgt0  11331  resqrexlemoverl  11332  resqrexlemglsq  11333  resqrexlemsqa  11335  resqrexlemex  11336  maxleastlt  11526  minmax  11541  lemininf  11545  ltmininf  11546  xrmaxleastlt  11567  xrmaxltsup  11569  xrminmax  11576  xrmin1inf  11578  xrmin2inf  11579  xrltmininf  11581  xrlemininf  11582  climserle  11656  summodclem3  11691  summodclem2a  11692  summodc  11694  zsumdc  11695  fsum3  11698  fsum00  11773  fsumabs  11776  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  zproddc  11890  fprodseq  11894  fprodle  11951  sin01bnd  12068  cos01bnd  12069  summodnegmod  12133  modmulconst  12134  dvdsaddr  12148  dvdssub  12149  dvdssubr  12150  dvdslelemd  12154  dvdsfac  12171  dvdsmod  12173  oddp1even  12187  ltoddhalfle  12204  opoe  12206  omoe  12207  divalg2  12237  divalgmod  12238  ndvdssub  12241  ndvdsadd  12242  bitsfval  12253  bitsval  12254  bits0  12259  bitsp1  12262  bitsfzolem  12265  bitsfzo  12266  bitscmp  12269  bitsinv1lem  12272  bezoutlembi  12326  dvdssqim  12345  dvdsmulgcd  12346  dvdssq  12352  nn0seqcvgd  12363  coprmdvds  12414  coprmdvds2  12415  rpmul  12420  cncongr1  12425  divgcdodd  12465  isprm6  12469  prmdvdsexp  12470  prmdvdsexpr  12472  prmfac1  12474  oddpwdclemxy  12491  oddpwdclemodd  12494  sqpweven  12497  2sqpwodd  12498  sqne2sq  12499  hashdvds  12543  phiprmpw  12544  eulerthlemh  12553  prmdiv  12557  prmdiveq  12558  odzval  12564  odzcllem  12565  odzdvds  12568  pythagtriplem11  12597  pythagtriplem13  12599  pythagtrip  12606  pceulem  12617  pczndvds2  12641  pcdvdsb  12643  pc2dvds  12653  pcz  12655  pcprmpw2  12656  dvdsprmpweq  12658  dvdsprmpweqle  12660  difsqpwdvds  12661  pcmpt  12666  prmpwdvds  12678  pockthlem  12679  4sqlem11  12724  exmidunben  12797  nninfdclemlt  12822  mulgval  13458  dvdsrtr  13863  dvdsrmul1  13864  unitnegcl  13892  unitpropdg  13910  elrhmunit  13939  zndvds0  14412  znunit  14421  mplsubgfilemcl  14461  psmettri2  14800  ismet2  14826  xmettri2  14833  comet  14971  ivthinclemum  15107  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemdisj  15112  ivthinclemloc  15113  ivthinc  15115  ivthreinc  15117  limccl  15131  ellimc3apf  15132  sin0pilem2  15254  pilem3  15255  sincosq1sgn  15298  sincosq2sgn  15299  sincosq4sgn  15301  logltb  15346  logle1b  15364  loglt1b  15365  logbgt0b  15438  wilthlem1  15452  sgmval  15455  dvdsppwf1o  15461  perfect1  15470  lgslem1  15477  lgsval  15481  lgsdilem  15504  lgsne0  15515  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  lgseisenlem1  15547  lgseisenlem2  15548  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem2  15559  m1lgs  15562  2lgslem1a1  15563  2lgslem1a  15565  2lgsoddprmlem2  15583  2lgsoddprmlem3  15588  2sqlem4  15595  2sqlem8a  15599