Theorem breq1d 4054

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
breq1d	⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Proof of Theorem breq1d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq1 4047	. 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:  eqnbrtrd  4062  eqbrtrd  4066  eqbrtrdi  4083  sbcbr2g  4101  pofun  4359  fmptco  5746  isorel  5877  isocnv  5880  isotr  5885  imbrov2fvoveq  5969  caovordig  6112  caovordg  6114  caovord  6118  xporderlem  6317  reldmtpos  6339  brtposg  6340  tpostpos  6350  tposoprab  6366  th3qlem2  6725  ensn1g  6889  fndmeng  6902  xpsneng  6917  xpcomco  6921  snnen2oprc  6957  tridc  6996  fimax2gtrilemstep  6997  unsnfidcel  7018  pm54.43  7298  ccfunen  7376  ltsonq  7511  ltanqg  7513  ltmnqg  7514  archnqq  7530  prloc  7604  addnqprulem  7641  appdivnq  7676  mulnqpru  7682  mullocprlem  7683  1idpru  7704  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdfl  7768  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlem2  7773  cauappcvgprlemlim  7774  cauappcvgpr  7775  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgprlem2  7793  caucvgpr  7795  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnkltj  7802  caucvgprprlemnkeqj  7803  caucvgprprlemnbj  7806  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  caucvgprprlemexb  7820  caucvgprprlemaddq  7821  caucvgprprlem1  7822  caucvgprprlem2  7823  ltsosr  7877  ltasrg  7883  addgt0sr  7888  mulextsr1  7894  prsrlt  7900  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  caucvgsr  7915  ltpsrprg  7916  pitonnlem2  7960  pitonn  7961  recidpipr  7969  axpre-ltadd  7999  axpre-mulext  8001  nntopi  8007  axcaucvglemval  8010  axcaucvglemcau  8011  axcaucvglemres  8012  ltaddnegr  8498  ltsubadd  8505  lesubadd  8507  ltaddsub2  8510  leaddsub2  8512  ltaddpos  8525  lesub2  8530  ltsub2  8532  ltnegcon2  8537  lenegcon2  8540  addge01  8545  subge0  8548  suble0  8549  lesub0  8552  ltordlem  8555  apreap  8660  divap0b  8756  mulgt1  8936  ltmulgt11  8937  gt0div  8943  ge0div  8944  ltmuldiv  8947  ltmuldiv2  8948  lemuldiv2  8955  ltrec  8956  lerec2  8962  ltdiv23  8965  lediv23  8966  sup3exmid  9030  addltmul  9274  avglt1  9276  avgle1  9278  div4p1lem1div2  9291  ztri3or  9415  zlem1lt  9429  zgt0ge1  9431  qapne  9760  irrmulap  9769  divlt1lt  9846  divle1le  9847  xrltso  9918  xltnegi  9957  xltadd1  9998  xposdif  10004  xlesubadd  10005  xleaddadd  10009  nn0disj  10260  qavgle  10401  fldiv4lem1div2uz2  10449  frec2uzf1od  10551  iseqf1olemfvp  10655  seqf1oglem1  10664  exp3vallem  10685  expap0  10714  leexp2r  10738  sqap0  10751  nn0ltexp2  10854  nn0opthlem1d  10865  hashennnuni  10924  hashunlem  10949  zfz1isolemiso  10984  seq3coll  10987  shftfvalg  11129  shftfibg  11131  shftfval  11132  shftfib  11134  shftfn  11135  2shfti  11142  shftidt2  11143  caucvgre  11292  cvg1nlemcau  11295  cvg1nlemres  11296  resqrexlemdecn  11323  resqrexlemoverl  11332  resqrexlemglsq  11333  resqrexlemsqa  11335  resqrexlemex  11336  abs00ap  11373  absdiflt  11403  absdifle  11404  lenegsq  11406  cau3lem  11425  minmax  11541  xrmaxltsup  11569  xrminmax  11576  xrltmininf  11581  xrlemininf  11582  clim  11592  clim2  11594  clim0  11596  clim0c  11597  climi0  11600  climuni  11604  2clim  11612  climshftlemg  11613  climshft  11615  climabs0  11618  climcn1  11619  climcn2  11620  addcn2  11621  subcn2  11622  mulcn2  11623  iser3shft  11657  climcau  11658  serf0  11663  sumeq1  11666  sumeq2  11670  sumrbdc  11690  summodclem2  11693  summodc  11694  zsumdc  11695  isumshft  11801  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  prodfap0  11856  prodfrecap  11857  prodfdivap  11858  ntrivcvgap  11859  ntrivcvgap0  11860  prodeq1f  11863  prodeq2w  11867  prodeq2  11868  prodrbdclem2  11884  prodmodclem2  11888  prodmodc  11889  zproddc  11890  fprodntrivap  11895  fprodap0  11932  fprodrec  11940  fproddivapf  11942  fprodap0f  11947  tanaddaplem  12049  sin01bnd  12068  cos01bnd  12069  halfleoddlt  12205  gcddvds  12284  dvdssq  12352  lcmgcdlem  12399  lcmdvds  12401  isprm  12431  prmgt1  12454  isprm5lem  12463  isprm6  12469  pw2dvdslemn  12487  pw2dvdseu  12490  oddpwdclemxy  12491  oddpwdclemndvds  12493  oddpwdclemodd  12494  odzdvds  12568  pclem0  12609  pclemub  12610  pclemdc  12611  pcprecl  12612  pcprendvds  12613  pcpremul  12616  pceulem  12617  pcval  12619  pcelnn  12644  pc2dvds  12653  pcadd  12663  pcadd2  12664  pcmpt  12666  prmpwdvds  12678  4sqlem17  12730  imasaddfnlemg  13146  znf1o  14413  znidomb  14420  mplsubgfilemm  14460  mplsubgfilemcl  14461  blfvalps  14857  elblps  14862  elbl  14863  elbl3ps  14866  elbl3  14867  blres  14906  comet  14971  bdbl  14975  xmetxp  14979  xmetxpbl  14980  metcnp2  14985  txmetcnp  14990  cnbl0  15006  cnblcld  15007  bl2ioo  15022  addcncntoplem  15033  divcnap  15037  mpomulcn  15038  elcncf  15045  elcncf2  15046  cncfi  15050  rescncf  15053  mulc1cncf  15061  cncfco  15063  cncfmet  15064  cncfmptid  15069  addccncf  15072  cdivcncfap  15076  negcncf  15077  mulcncflem  15079  mulcncf  15080  ivthinclemlm  15106  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemdisj  15112  ivthinclemloc  15113  ivthinc  15115  ivthreinc  15117  limccl  15131  ellimc3apf  15132  limcdifap  15134  limcmpted  15135  limcimolemlt  15136  limcresi  15138  cnplimcim  15139  limccnpcntop  15147  limccnp2lem  15148  limccoap  15150  dvcoapbr  15179  dveflem  15198  eflt  15247  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  logltb  15346  logge0b  15362  loggt0b  15363  lgslem2  15478  lgslem3  15479  lgsval  15481  lgsfcl2  15483  lgsfle1  15486  lgsle1  15492  lgsdirprm  15511  lgsne0  15515  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem2  15539  gausslemma2dlem3  15540  gausslemma2dlem4  15541  qdencn  15966  trilpolemlt1  15980