Theorem breq1d 4098

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 4091	. 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:  eqnbrtrd  4106  eqbrtrd  4110  eqbrtrdi  4127  sbcbr2g  4146  pofun  4409  fmptco  5813  isorel  5949  isocnv  5952  isotr  5957  imbrov2fvoveq  6043  caovordig  6188  caovordg  6190  caovord  6194  xporderlem  6396  reldmtpos  6419  brtposg  6420  tpostpos  6430  tposoprab  6446  th3qlem2  6807  ensn1g  6971  fndmeng  6985  xpsneng  7006  xpcomco  7010  snnen2oprc  7046  tridc  7089  fimax2gtrilemstep  7090  unsnfidcel  7113  pm54.43  7395  pr1or2  7399  ccfunen  7483  ltsonq  7618  ltanqg  7620  ltmnqg  7621  archnqq  7637  prloc  7711  addnqprulem  7748  appdivnq  7783  mulnqpru  7789  mullocprlem  7790  1idpru  7811  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlem2  7880  cauappcvgprlemlim  7881  cauappcvgpr  7882  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprlem2  7900  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnbj  7913  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlemexb  7927  caucvgprprlemaddq  7928  caucvgprprlem1  7929  caucvgprprlem2  7930  ltsosr  7984  ltasrg  7990  addgt0sr  7995  mulextsr1  8001  prsrlt  8007  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  caucvgsr  8022  ltpsrprg  8023  pitonnlem2  8067  pitonn  8068  recidpipr  8076  axpre-ltadd  8106  axpre-mulext  8108  nntopi  8114  axcaucvglemval  8117  axcaucvglemcau  8118  axcaucvglemres  8119  ltaddnegr  8605  ltsubadd  8612  lesubadd  8614  ltaddsub2  8617  leaddsub2  8619  ltaddpos  8632  lesub2  8637  ltsub2  8639  ltnegcon2  8644  lenegcon2  8647  addge01  8652  subge0  8655  suble0  8656  lesub0  8659  ltordlem  8662  apreap  8767  divap0b  8863  mulgt1  9043  ltmulgt11  9044  gt0div  9050  ge0div  9051  ltmuldiv  9054  ltmuldiv2  9055  lemuldiv2  9062  ltrec  9063  lerec2  9069  ltdiv23  9072  lediv23  9073  sup3exmid  9137  addltmul  9381  avglt1  9383  avgle1  9385  div4p1lem1div2  9398  ztri3or  9522  zlem1lt  9536  zgt0ge1  9538  qapne  9873  irrmulap  9882  divlt1lt  9959  divle1le  9960  xrltso  10031  xltnegi  10070  xltadd1  10111  xposdif  10117  xlesubadd  10118  xleaddadd  10122  nn0disj  10373  qavgle  10519  fldiv4lem1div2uz2  10567  frec2uzf1od  10669  iseqf1olemfvp  10773  seqf1oglem1  10782  exp3vallem  10803  expap0  10832  leexp2r  10856  sqap0  10869  nn0ltexp2  10972  nn0opthlem1d  10983  hashennnuni  11042  hashunlem  11068  zfz1isolemiso  11104  seq3coll  11107  swrdccatin2  11314  shftfvalg  11396  shftfibg  11398  shftfval  11399  shftfib  11401  shftfn  11402  2shfti  11409  shftidt2  11410  caucvgre  11559  cvg1nlemcau  11562  cvg1nlemres  11563  resqrexlemdecn  11590  resqrexlemoverl  11599  resqrexlemglsq  11600  resqrexlemsqa  11602  resqrexlemex  11603  abs00ap  11640  absdiflt  11670  absdifle  11671  lenegsq  11673  cau3lem  11692  minmax  11808  xrmaxltsup  11836  xrminmax  11843  xrltmininf  11848  xrlemininf  11849  clim  11859  clim2  11861  clim0  11863  clim0c  11864  climi0  11867  climuni  11871  2clim  11879  climshftlemg  11880  climshft  11882  climabs0  11885  climcn1  11886  climcn2  11887  addcn2  11888  subcn2  11889  mulcn2  11890  iser3shft  11924  climcau  11925  serf0  11930  sumeq1  11933  sumeq2  11937  sumrbdc  11958  summodclem2  11961  summodc  11962  zsumdc  11963  isumshft  12069  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  prodfap0  12124  prodfrecap  12125  prodfdivap  12126  ntrivcvgap  12127  ntrivcvgap0  12128  prodeq1f  12131  prodeq2w  12135  prodeq2  12136  prodrbdclem2  12152  prodmodclem2  12156  prodmodc  12157  zproddc  12158  fprodntrivap  12163  fprodap0  12200  fprodrec  12208  fproddivapf  12210  fprodap0f  12215  tanaddaplem  12317  sin01bnd  12336  cos01bnd  12337  halfleoddlt  12473  gcddvds  12552  dvdssq  12620  lcmgcdlem  12667  lcmdvds  12669  isprm  12699  prmgt1  12722  isprm5lem  12731  isprm6  12737  pw2dvdslemn  12755  pw2dvdseu  12758  oddpwdclemxy  12759  oddpwdclemndvds  12761  oddpwdclemodd  12762  odzdvds  12836  pclem0  12877  pclemub  12878  pclemdc  12879  pcprecl  12880  pcprendvds  12881  pcpremul  12884  pceulem  12885  pcval  12887  pcelnn  12912  pc2dvds  12921  pcadd  12931  pcadd2  12932  pcmpt  12934  prmpwdvds  12946  4sqlem17  12998  imasaddfnlemg  13415  znf1o  14684  znidomb  14691  mplsubgfilemm  14731  mplsubgfilemcl  14732  blfvalps  15128  elblps  15133  elbl  15134  elbl3ps  15137  elbl3  15138  blres  15177  comet  15242  bdbl  15246  xmetxp  15250  xmetxpbl  15251  metcnp2  15256  txmetcnp  15261  cnbl0  15277  cnblcld  15278  bl2ioo  15293  addcncntoplem  15304  divcnap  15308  mpomulcn  15309  elcncf  15316  elcncf2  15317  cncfi  15321  rescncf  15324  mulc1cncf  15332  cncfco  15334  cncfmet  15335  cncfmptid  15340  addccncf  15343  cdivcncfap  15347  negcncf  15348  mulcncflem  15350  mulcncf  15351  ivthinclemlm  15377  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemdisj  15383  ivthinclemloc  15384  ivthinc  15386  ivthreinc  15388  limccl  15402  ellimc3apf  15403  limcdifap  15405  limcmpted  15406  limcimolemlt  15407  limcresi  15409  cnplimcim  15410  limccnpcntop  15418  limccnp2lem  15419  limccoap  15421  dvcoapbr  15450  dveflem  15469  eflt  15518  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  logltb  15617  logge0b  15633  loggt0b  15634  lgslem2  15749  lgslem3  15750  lgsval  15752  lgsfcl2  15754  lgsfle1  15757  lgsle1  15763  lgsdirprm  15782  lgsne0  15786  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem2  15810  gausslemma2dlem3  15811  gausslemma2dlem4  15812  subupgr  16143  vtxdumgrfival  16168  qdencn  16682  trilpolemlt1  16696