Theorem breq1d 4008

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   class class class wbr 3998

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999

This theorem is referenced by:  eqnbrtrd  4016  eqbrtrd  4020  eqbrtrdi  4037  sbcbr2g  4055  pofun  4306  fmptco  5674  isorel  5799  isocnv  5802  isotr  5807  imbrov2fvoveq  5890  caovordig  6030  caovordg  6032  caovord  6036  xporderlem  6222  reldmtpos  6244  brtposg  6245  tpostpos  6255  tposoprab  6271  th3qlem2  6628  ensn1g  6787  fndmeng  6800  xpsneng  6812  xpcomco  6816  snnen2oprc  6850  tridc  6889  fimax2gtrilemstep  6890  unsnfidcel  6910  pm54.43  7179  ccfunen  7238  ltsonq  7372  ltanqg  7374  ltmnqg  7375  archnqq  7391  prloc  7465  addnqprulem  7502  appdivnq  7537  mulnqpru  7543  mullocprlem  7544  1idpru  7565  cauappcvgprlemm  7619  cauappcvgprlemopl  7620  cauappcvgprlemlol  7621  cauappcvgprlemdisj  7625  cauappcvgprlemloc  7626  cauappcvgprlemladdfl  7629  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  cauappcvgprlem1  7633  cauappcvgprlem2  7634  cauappcvgprlemlim  7635  cauappcvgpr  7636  caucvgprlemnkj  7640  caucvgprlemnbj  7641  caucvgprlemm  7642  caucvgprlemopl  7643  caucvgprlemlol  7644  caucvgprlemdisj  7648  caucvgprlemloc  7649  caucvgprlemcl  7650  caucvgprlemladdfu  7651  caucvgprlemladdrl  7652  caucvgprlem1  7653  caucvgprlem2  7654  caucvgpr  7656  caucvgprprlemell  7659  caucvgprprlemelu  7660  caucvgprprlemcbv  7661  caucvgprprlemval  7662  caucvgprprlemnkltj  7663  caucvgprprlemnkeqj  7664  caucvgprprlemnbj  7667  caucvgprprlemml  7668  caucvgprprlemmu  7669  caucvgprprlemopl  7671  caucvgprprlemlol  7672  caucvgprprlemopu  7673  caucvgprprlemloc  7677  caucvgprprlemclphr  7679  caucvgprprlemexbt  7680  caucvgprprlemexb  7681  caucvgprprlemaddq  7682  caucvgprprlem1  7683  caucvgprprlem2  7684  ltsosr  7738  ltasrg  7744  addgt0sr  7749  mulextsr1  7755  prsrlt  7761  caucvgsrlemgt1  7769  caucvgsrlemoffres  7774  caucvgsr  7776  ltpsrprg  7777  pitonnlem2  7821  pitonn  7822  recidpipr  7830  axpre-ltadd  7860  axpre-mulext  7862  nntopi  7868  axcaucvglemval  7871  axcaucvglemcau  7872  axcaucvglemres  7873  ltaddnegr  8356  ltsubadd  8363  lesubadd  8365  ltaddsub2  8368  leaddsub2  8370  ltaddpos  8383  lesub2  8388  ltsub2  8390  ltnegcon2  8395  lenegcon2  8398  addge01  8403  subge0  8406  suble0  8407  lesub0  8410  ltordlem  8413  apreap  8518  divap0b  8612  mulgt1  8791  ltmulgt11  8792  gt0div  8798  ge0div  8799  ltmuldiv  8802  ltmuldiv2  8803  lemuldiv2  8810  ltrec  8811  lerec2  8817  ltdiv23  8820  lediv23  8821  sup3exmid  8885  addltmul  9126  avglt1  9128  avgle1  9130  div4p1lem1div2  9143  ztri3or  9267  zlem1lt  9280  zgt0ge1  9282  qapne  9610  divlt1lt  9693  divle1le  9694  xrltso  9765  xltnegi  9804  xltadd1  9845  xposdif  9851  xlesubadd  9852  xleaddadd  9856  nn0disj  10106  qavgle  10227  frec2uzf1od  10374  iseqf1olemfvp  10465  exp3vallem  10489  expap0  10518  leexp2r  10542  sqap0  10554  nn0ltexp2  10656  nn0opthlem1d  10666  hashennnuni  10725  hashunlem  10750  zfz1isolemiso  10785  seq3coll  10788  shftfvalg  10793  shftfibg  10795  shftfval  10796  shftfib  10798  shftfn  10799  2shfti  10806  shftidt2  10807  caucvgre  10956  cvg1nlemcau  10959  cvg1nlemres  10960  resqrexlemdecn  10987  resqrexlemoverl  10996  resqrexlemglsq  10997  resqrexlemsqa  10999  resqrexlemex  11000  abs00ap  11037  absdiflt  11067  absdifle  11068  lenegsq  11070  cau3lem  11089  minmax  11204  xrmaxltsup  11232  xrminmax  11239  xrltmininf  11244  xrlemininf  11245  clim  11255  clim2  11257  clim0  11259  clim0c  11260  climi0  11263  climuni  11267  2clim  11275  climshftlemg  11276  climshft  11278  climabs0  11281  climcn1  11282  climcn2  11283  addcn2  11284  subcn2  11285  mulcn2  11286  iser3shft  11320  climcau  11321  serf0  11326  sumeq1  11329  sumeq2  11333  sumrbdc  11353  summodclem2  11356  summodc  11357  zsumdc  11358  isumshft  11464  mertenslemi1  11509  mertenslem2  11510  mertensabs  11511  prodfap0  11519  prodfrecap  11520  prodfdivap  11521  ntrivcvgap  11522  ntrivcvgap0  11523  prodeq1f  11526  prodeq2w  11530  prodeq2  11531  prodrbdclem2  11547  prodmodclem2  11551  prodmodc  11552  zproddc  11553  fprodntrivap  11558  fprodap0  11595  fprodrec  11603  fproddivapf  11605  fprodap0f  11610  tanaddaplem  11712  sin01bnd  11731  cos01bnd  11732  halfleoddlt  11864  gcddvds  11929  dvdssq  11997  lcmgcdlem  12042  lcmdvds  12044  isprm  12074  prmgt1  12097  isprm5lem  12106  isprm6  12112  pw2dvdslemn  12130  pw2dvdseu  12133  oddpwdclemxy  12134  oddpwdclemndvds  12136  oddpwdclemodd  12137  odzdvds  12210  pclem0  12251  pclemub  12252  pclemdc  12253  pcprecl  12254  pcprendvds  12255  pcpremul  12258  pceulem  12259  pcval  12261  pcelnn  12285  pc2dvds  12294  pcadd  12304  pcmpt  12306  prmpwdvds  12318  blfvalps  13454  elblps  13459  elbl  13460  elbl3ps  13463  elbl3  13464  blres  13503  comet  13568  bdbl  13572  xmetxp  13576  xmetxpbl  13577  metcnp2  13582  txmetcnp  13587  cnbl0  13603  cnblcld  13604  bl2ioo  13611  addcncntoplem  13620  divcnap  13624  elcncf  13629  elcncf2  13630  cncfi  13634  rescncf  13637  mulc1cncf  13645  cncfco  13647  cncfmet  13648  cncfmptid  13652  addccncf  13655  cdivcncfap  13656  negcncf  13657  mulcncflem  13659  mulcncf  13660  ivthinclemlm  13681  ivthinclemlopn  13683  ivthinclemlr  13684  ivthinclemuopn  13685  ivthinclemur  13686  ivthinclemdisj  13687  ivthinclemloc  13688  ivthinc  13690  limccl  13697  ellimc3apf  13698  limcdifap  13700  limcmpted  13701  limcimolemlt  13702  limcresi  13704  cnplimcim  13705  limccnpcntop  13713  limccnp2lem  13714  limccoap  13716  dvcoapbr  13740  dveflem  13756  eflt  13765  sincosq2sgn  13817  sincosq3sgn  13818  sincosq4sgn  13819  logltb  13864  logge0b  13880  loggt0b  13881  lgslem2  13971  lgslem3  13972  lgsval  13974  lgsfcl2  13976  lgsfle1  13979  lgsle1  13985  lgsdirprm  14004  lgsne0  14008  qdencn  14334  trilpolemlt1  14348