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  5948  isocnv  5951  isotr  5956  imbrov2fvoveq  6042  caovordig  6187  caovordg  6189  caovord  6193  xporderlem  6395  reldmtpos  6418  brtposg  6419  tpostpos  6429  tposoprab  6445  th3qlem2  6806  ensn1g  6970  fndmeng  6984  xpsneng  7005  xpcomco  7009  snnen2oprc  7045  tridc  7088  fimax2gtrilemstep  7089  unsnfidcel  7112  pm54.43  7394  pr1or2  7398  ccfunen  7482  ltsonq  7617  ltanqg  7619  ltmnqg  7620  archnqq  7636  prloc  7710  addnqprulem  7747  appdivnq  7782  mulnqpru  7788  mullocprlem  7789  1idpru  7810  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlem2  7879  cauappcvgprlemlim  7880  cauappcvgpr  7881  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem1  7898  caucvgprlem2  7899  caucvgpr  7901  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemnkltj  7908  caucvgprprlemnkeqj  7909  caucvgprprlemnbj  7912  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  caucvgprprlemexb  7926  caucvgprprlemaddq  7927  caucvgprprlem1  7928  caucvgprprlem2  7929  ltsosr  7983  ltasrg  7989  addgt0sr  7994  mulextsr1  8000  prsrlt  8006  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  caucvgsr  8021  ltpsrprg  8022  pitonnlem2  8066  pitonn  8067  recidpipr  8075  axpre-ltadd  8105  axpre-mulext  8107  nntopi  8113  axcaucvglemval  8116  axcaucvglemcau  8117  axcaucvglemres  8118  ltaddnegr  8604  ltsubadd  8611  lesubadd  8613  ltaddsub2  8616  leaddsub2  8618  ltaddpos  8631  lesub2  8636  ltsub2  8638  ltnegcon2  8643  lenegcon2  8646  addge01  8651  subge0  8654  suble0  8655  lesub0  8658  ltordlem  8661  apreap  8766  divap0b  8862  mulgt1  9042  ltmulgt11  9043  gt0div  9049  ge0div  9050  ltmuldiv  9053  ltmuldiv2  9054  lemuldiv2  9061  ltrec  9062  lerec2  9068  ltdiv23  9071  lediv23  9072  sup3exmid  9136  addltmul  9380  avglt1  9382  avgle1  9384  div4p1lem1div2  9397  ztri3or  9521  zlem1lt  9535  zgt0ge1  9537  qapne  9872  irrmulap  9881  divlt1lt  9958  divle1le  9959  xrltso  10030  xltnegi  10069  xltadd1  10110  xposdif  10116  xlesubadd  10117  xleaddadd  10121  nn0disj  10372  qavgle  10517  fldiv4lem1div2uz2  10565  frec2uzf1od  10667  iseqf1olemfvp  10771  seqf1oglem1  10780  exp3vallem  10801  expap0  10830  leexp2r  10854  sqap0  10867  nn0ltexp2  10970  nn0opthlem1d  10981  hashennnuni  11040  hashunlem  11066  zfz1isolemiso  11102  seq3coll  11105  swrdccatin2  11309  shftfvalg  11378  shftfibg  11380  shftfval  11381  shftfib  11383  shftfn  11384  2shfti  11391  shftidt2  11392  caucvgre  11541  cvg1nlemcau  11544  cvg1nlemres  11545  resqrexlemdecn  11572  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemsqa  11584  resqrexlemex  11585  abs00ap  11622  absdiflt  11652  absdifle  11653  lenegsq  11655  cau3lem  11674  minmax  11790  xrmaxltsup  11818  xrminmax  11825  xrltmininf  11830  xrlemininf  11831  clim  11841  clim2  11843  clim0  11845  clim0c  11846  climi0  11849  climuni  11853  2clim  11861  climshftlemg  11862  climshft  11864  climabs0  11867  climcn1  11868  climcn2  11869  addcn2  11870  subcn2  11871  mulcn2  11872  iser3shft  11906  climcau  11907  serf0  11912  sumeq1  11915  sumeq2  11919  sumrbdc  11939  summodclem2  11942  summodc  11943  zsumdc  11944  isumshft  12050  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  prodfap0  12105  prodfrecap  12106  prodfdivap  12107  ntrivcvgap  12108  ntrivcvgap0  12109  prodeq1f  12112  prodeq2w  12116  prodeq2  12117  prodrbdclem2  12133  prodmodclem2  12137  prodmodc  12138  zproddc  12139  fprodntrivap  12144  fprodap0  12181  fprodrec  12189  fproddivapf  12191  fprodap0f  12196  tanaddaplem  12298  sin01bnd  12317  cos01bnd  12318  halfleoddlt  12454  gcddvds  12533  dvdssq  12601  lcmgcdlem  12648  lcmdvds  12650  isprm  12680  prmgt1  12703  isprm5lem  12712  isprm6  12718  pw2dvdslemn  12736  pw2dvdseu  12739  oddpwdclemxy  12740  oddpwdclemndvds  12742  oddpwdclemodd  12743  odzdvds  12817  pclem0  12858  pclemub  12859  pclemdc  12860  pcprecl  12861  pcprendvds  12862  pcpremul  12865  pceulem  12866  pcval  12868  pcelnn  12893  pc2dvds  12902  pcadd  12912  pcadd2  12913  pcmpt  12915  prmpwdvds  12927  4sqlem17  12979  imasaddfnlemg  13396  znf1o  14664  znidomb  14671  mplsubgfilemm  14711  mplsubgfilemcl  14712  blfvalps  15108  elblps  15113  elbl  15114  elbl3ps  15117  elbl3  15118  blres  15157  comet  15222  bdbl  15226  xmetxp  15230  xmetxpbl  15231  metcnp2  15236  txmetcnp  15241  cnbl0  15257  cnblcld  15258  bl2ioo  15273  addcncntoplem  15284  divcnap  15288  mpomulcn  15289  elcncf  15296  elcncf2  15297  cncfi  15301  rescncf  15304  mulc1cncf  15312  cncfco  15314  cncfmet  15315  cncfmptid  15320  addccncf  15323  cdivcncfap  15327  negcncf  15328  mulcncflem  15330  mulcncf  15331  ivthinclemlm  15357  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemdisj  15363  ivthinclemloc  15364  ivthinc  15366  ivthreinc  15368  limccl  15382  ellimc3apf  15383  limcdifap  15385  limcmpted  15386  limcimolemlt  15387  limcresi  15389  cnplimcim  15390  limccnpcntop  15398  limccnp2lem  15399  limccoap  15401  dvcoapbr  15430  dveflem  15449  eflt  15498  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  logltb  15597  logge0b  15613  loggt0b  15614  lgslem2  15729  lgslem3  15730  lgsval  15732  lgsfcl2  15734  lgsfle1  15737  lgsle1  15743  lgsdirprm  15762  lgsne0  15766  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem2  15790  gausslemma2dlem3  15791  gausslemma2dlem4  15792  subupgr  16123  vtxdumgrfival  16148  qdencn  16631  trilpolemlt1  16645