Theorem breq2d 4055

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372   class class class wbr 4043

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044

This theorem is referenced by:  breqtrd  4069  sbcbr1g  4099  pofun  4358  csbfv12g  5613  isorel  5876  isocnv  5879  isotr  5884  caovordig  6111  caovordg  6113  caovord  6117  xporderlem  6316  th3qlem2  6724  phplem3g  6952  supsnti  7106  inflbti  7125  difinfinf  7202  enqdc1  7474  ltanqg  7512  ltmnqg  7513  archnqq  7529  prarloclemarch2  7531  prloc  7603  addnqprllem  7639  addlocprlemgt  7646  appdivnq  7675  mulnqprl  7680  1idprl  7702  ltexprlemloc  7719  caucvgprlemcanl  7756  cauappcvgprlemm  7757  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  cauappcvgprlemlim  7773  cauappcvgpr  7774  archrecnq  7775  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemcl  7788  caucvgprlemladdrl  7790  caucvgpr  7794  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemnkeqj  7802  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexbt  7818  caucvgprprlem1  7821  caucvgprprlem2  7822  caucvgprpr  7824  ltposr  7875  ltasrg  7882  mulgt0sr  7890  mulextsr1lem  7892  mulextsr1  7893  prsrlt  7899  caucvgsrlemcl  7901  caucvgsrlemfv  7903  caucvgsrlembound  7906  caucvgsrlemgt1  7907  caucvgsrlemoffres  7912  caucvgsr  7914  map2psrprg  7917  pitonnlem2  7959  pitonn  7960  recidpipr  7968  axpre-ltadd  7998  axpre-mulgt0  7999  axpre-mulext  8000  axarch  8003  nntopi  8006  axcaucvglemval  8009  axcaucvglemcau  8010  axcaucvglemres  8011  axpre-suploclemres  8013  ltaddneg  8496  ltsubadd2  8505  lesubadd2  8507  ltaddsub  8508  leaddsub  8510  ltaddpos2  8525  posdif  8527  lesub1  8528  ltsub1  8530  ltnegcon1  8535  lenegcon1  8538  addge02  8545  leaddle0  8549  ltordlem  8554  possumd  8641  sublt0d  8642  apreap  8659  prodgt02  8925  prodge02  8927  ltmulgt12  8937  lemulge12  8939  ltdivmul  8948  ledivmul  8949  ltdivmul2  8950  lt2mul2div  8951  ledivmul2  8952  ltrec  8955  ltrec1  8960  ltdiv23  8964  lediv23  8965  nnge1  9058  halfpos  9267  lt2halves  9272  addltmul  9273  avglt2  9276  avgle2  9278  nnrecl  9292  zltlem1  9429  difgtsumgt  9441  nn0le2is012  9454  gtndiv  9467  qapne  9759  nnledivrp  9887  xltnegi  9956  xltadd1  9997  xsubge0  10002  xposdif  10003  xlesubadd  10004  xleaddadd  10008  divelunit  10123  eluzgtdifelfzo  10324  qtri3or  10381  exbtwnzlemstep  10388  exbtwnzlemshrink  10389  exbtwnzlemex  10390  exbtwnz  10391  rebtwn2zlemstep  10393  rebtwn2zlemshrink  10394  rebtwn2z  10395  flqlelt  10417  flqbi  10431  2tnp1ge0ge0  10442  q2submod  10528  frec2uzltd  10546  frec2uzlt2d  10547  frec2uzf1od  10549  monoord  10628  ser3mono  10630  ser3ge0  10679  expnbnd  10806  nn0ltexp2  10852  facwordi  10883  hashunlem  10947  zfz1isolemiso  10982  seq3coll  10985  caucvgrelemcau  11262  caucvgre  11263  cvg1nlemcau  11266  cvg1nlemres  11267  recvguniq  11277  resqrexlemover  11292  resqrexlemgt0  11302  resqrexlemoverl  11303  resqrexlemglsq  11304  resqrexlemsqa  11306  resqrexlemex  11307  maxleastlt  11497  minmax  11512  lemininf  11516  ltmininf  11517  xrmaxleastlt  11538  xrmaxltsup  11540  xrminmax  11547  xrmin1inf  11549  xrmin2inf  11550  xrltmininf  11552  xrlemininf  11553  climserle  11627  summodclem3  11662  summodclem2a  11663  summodc  11665  zsumdc  11666  fsum3  11669  fsum00  11744  fsumabs  11747  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  zproddc  11861  fprodseq  11865  fprodle  11922  sin01bnd  12039  cos01bnd  12040  summodnegmod  12104  modmulconst  12105  dvdsaddr  12119  dvdssub  12120  dvdssubr  12121  dvdslelemd  12125  dvdsfac  12142  dvdsmod  12144  oddp1even  12158  ltoddhalfle  12175  opoe  12177  omoe  12178  divalg2  12208  divalgmod  12209  ndvdssub  12212  ndvdsadd  12213  bitsfval  12224  bitsval  12225  bits0  12230  bitsp1  12233  bitsfzolem  12236  bitsfzo  12237  bitscmp  12240  bitsinv1lem  12243  bezoutlembi  12297  dvdssqim  12316  dvdsmulgcd  12317  dvdssq  12323  nn0seqcvgd  12334  coprmdvds  12385  coprmdvds2  12386  rpmul  12391  cncongr1  12396  divgcdodd  12436  isprm6  12440  prmdvdsexp  12441  prmdvdsexpr  12443  prmfac1  12445  oddpwdclemxy  12462  oddpwdclemodd  12465  sqpweven  12468  2sqpwodd  12469  sqne2sq  12470  hashdvds  12514  phiprmpw  12515  eulerthlemh  12524  prmdiv  12528  prmdiveq  12529  odzval  12535  odzcllem  12536  odzdvds  12539  pythagtriplem11  12568  pythagtriplem13  12570  pythagtrip  12577  pceulem  12588  pczndvds2  12612  pcdvdsb  12614  pc2dvds  12624  pcz  12626  pcprmpw2  12627  dvdsprmpweq  12629  dvdsprmpweqle  12631  difsqpwdvds  12632  pcmpt  12637  prmpwdvds  12649  pockthlem  12650  4sqlem11  12695  exmidunben  12768  nninfdclemlt  12793  mulgval  13429  dvdsrtr  13834  dvdsrmul1  13835  unitnegcl  13863  unitpropdg  13881  elrhmunit  13910  zndvds0  14383  znunit  14392  mplsubgfilemcl  14432  psmettri2  14771  ismet2  14797  xmettri2  14804  comet  14942  ivthinclemum  15078  ivthinclemlopn  15079  ivthinclemlr  15080  ivthinclemuopn  15081  ivthinclemur  15082  ivthinclemdisj  15083  ivthinclemloc  15084  ivthinc  15086  ivthreinc  15088  limccl  15102  ellimc3apf  15103  sin0pilem2  15225  pilem3  15226  sincosq1sgn  15269  sincosq2sgn  15270  sincosq4sgn  15272  logltb  15317  logle1b  15335  loglt1b  15336  logbgt0b  15409  wilthlem1  15423  sgmval  15426  dvdsppwf1o  15432  perfect1  15441  lgslem1  15448  lgsval  15452  lgsdilem  15475  lgsne0  15486  gausslemma2dlem1a  15506  gausslemma2dlem1f1o  15508  lgseisenlem1  15518  lgseisenlem2  15519  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527  lgsquad2lem2  15530  m1lgs  15533  2lgslem1a1  15534  2lgslem1a  15536  2lgsoddprmlem2  15554  2lgsoddprmlem3  15559  2sqlem4  15566  2sqlem8a  15570