Theorem breq1d 4141

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   class class class wbr 4131

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4132

This theorem is used by:  eqnbrtrd  4149  eqbrtrd  4153  eqbrtrdi  4170  sbcbr2g  4189  pofun  4459  fmptco  5877  isorel  6017  isocnv  6020  isotr  6025  imbrov2fvoveq  6113  caovordig  6258  caovordg  6260  caovord  6264  xporderlem  6471  reldmtpos  6528  brtposg  6529  tpostpos  6539  tposoprab  6555  th3qlem2  6916  ensn1g  7088  fndmeng  7102  xpsneng  7124  xpcomco  7128  snnen2oprc  7165  tridc  7208  fimax2gtrilemstep  7209  unsnfidcel  7232  pm54.43  7542  pr1or2  7546  ccfunen  7636  ltsonq  7771  ltanqg  7773  ltmnqg  7774  archnqq  7790  prloc  7864  addnqprulem  7901  appdivnq  7936  mulnqpru  7942  mullocprlem  7943  1idpru  7964  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlem2  8033  cauappcvgprlemlim  8034  cauappcvgpr  8035  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem1  8052  caucvgprlem2  8053  caucvgpr  8055  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemnbj  8066  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemopu  8072  caucvgprprlemloc  8076  caucvgprprlemclphr  8078  caucvgprprlemexbt  8079  caucvgprprlemexb  8080  caucvgprprlemaddq  8081  caucvgprprlem1  8082  caucvgprprlem2  8083  ltsosr  8137  ltasrg  8143  addgt0sr  8148  mulextsr1  8154  prsrlt  8160  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  caucvgsr  8175  ltpsrprg  8176  pitonnlem2  8220  pitonn  8221  recidpipr  8229  axpre-ltadd  8259  axpre-mulext  8261  nntopi  8267  axcaucvglemval  8270  axcaucvglemcau  8271  axcaucvglemres  8272  ltaddnegr  8760  ltsubadd  8767  lesubadd  8769  ltaddsub2  8772  leaddsub2  8774  ltaddpos  8787  lesub2  8792  ltsub2  8794  ltnegcon2  8799  lenegcon2  8802  addge01  8807  subge0  8810  suble0  8811  lesub0  8814  ltordlem  8817  apreap  8923  divap0b  9021  mulgt1  9201  ltmulgt11  9202  gt0div  9208  ge0div  9209  ltmuldiv  9212  ltmuldiv2  9213  lemuldiv2  9220  ltrec  9221  lerec2  9227  ltdiv23  9230  lediv23  9231  sup3exmid  9295  addltmul  9553  avglt1  9555  avgle1  9557  div4p1lem1div2  9570  ztri3or  9698  zlem1lt  9712  zgt0ge1  9714  qapne  10055  irrmulap  10065  divlt1lt  10142  divle1le  10143  xrltso  10215  xltnegi  10254  xltadd1  10295  xposdif  10301  xlesubadd  10302  xleaddadd  10306  nn0disj  10562  qavgle  10710  fldiv4lem1div2uz2  10762  frec2uzf1od  10864  iseqf1olemfvp  10968  seqf1oglem1  10977  exp3vallem  10998  expap0  11027  leexp2r  11051  sqap0  11064  nn0ltexp2  11169  nn0opthlem1d  11180  hashennnuni  11240  hashunlem  11266  hashf1  11309  zfz1isolemiso  11313  seq3coll  11316  swrdccatin2  11523  shftfvalg  11605  shftfibg  11607  shftfval  11608  shftfib  11610  shftfn  11611  2shfti  11618  shftidt2  11619  caucvgre  11769  cvg1nlemcau  11772  cvg1nlemres  11773  resqrexlemdecn  11800  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemsqa  11812  resqrexlemex  11813  abs00ap  11850  absdiflt  11881  absdifle  11882  lenegsq  11884  cau3lem  11903  fiidxsupcl  12018  minmax  12020  xrmaxltsup  12049  xrminmax  12056  xrltmininf  12061  xrlemininf  12062  clim  12072  clim2  12074  clim0  12076  clim0c  12077  climi0  12080  climuni  12084  2clim  12092  climshftlemg  12093  climshft  12095  climabs0  12098  climcn1  12099  climcn2  12100  addcn2  12101  subcn2  12102  mulcn2  12103  iser3shft  12137  climcau  12138  serf0  12143  sumeq1  12146  sumeq2  12150  sumrbdc  12171  summodclem2  12174  summodc  12175  zsumdc  12176  isumshft  12282  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  prodfap0  12337  prodfrecap  12338  prodfdivap  12339  ntrivcvgap  12340  ntrivcvgap0  12341  prodeq1f  12344  prodeq2w  12348  prodeq2  12349  prodrbdclem2  12365  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodntrivap  12376  fprodap0  12413  fprodrec  12421  fproddivapf  12423  fprodap0f  12428  tanaddaplem  12530  sin01bnd  12549  cos01bnd  12550  halfleoddlt  12686  gcddvds  12765  dvdssq  12833  lcmgcdlem  12880  lcmdvds  12882  isprm  12912  prmgt1  12936  isprm5lem  12945  isprm6  12951  pwbdvdslemn  12969  pwbdvdseu  12972  nnmaxpwlemxy  12973  nnmaxpwlemnfac  12976  sqrtrirr  13014  odzdvds  13053  pclem0  13094  pclemub  13095  pclemdc  13096  pcprecl  13097  pcprendvds  13098  pcpremul  13101  pceulem  13102  pcval  13104  pcelnn  13129  pc2dvds  13138  pcadd  13148  pcadd2  13149  pcmpt  13151  prmpwdvds  13163  4sqlem17  13215  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemodife  13298  ballotfilemic  13308  ballotfilemsv  13311  ballotfilemrc  13332  imasaddfnlemg  13694  znf1o  15095  znidomb  15102  psrbaglefifi  15172  mplsubgfilemm  15214  mplsubgfilemcl  15215  blfvalps  15611  elblps  15616  elbl  15617  elbl3ps  15620  elbl3  15621  blres  15660  comet  15725  bdbl  15729  xmetxp  15733  xmetxpbl  15734  metcnp2  15739  txmetcnp  15744  cnbl0  15760  cnblcld  15761  bl2ioo  15776  addcncntoplem  15787  divcnap  15791  mpomulcn  15792  elcncf  15799  elcncf2  15800  cncfi  15804  rescncf  15807  mulc1cncf  15815  cncfco  15817  cncfmet  15818  cncfmptid  15823  addccncf  15826  cdivcncfap  15830  negcncf  15831  mulcncflem  15833  mulcncf  15834  ivthinclemlm  15860  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemdisj  15866  ivthinclemloc  15867  ivthinc  15869  ivthreinc  15871  limccl  15885  ellimc3apf  15886  limcdifap  15888  limcmpted  15889  limcimolemlt  15890  limcresi  15892  cnplimcim  15893  limccnpcntop  15901  limccnp2lem  15902  limccoap  15904  dvcoapbr  15933  dveflem  15952  eflt  16001  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  logltb  16104  logge0b  16120  loggt0b  16121  zprmlogbaplem2  16216  zprmlogbap  16218  pellexlem3  16231  chtublem  16295  chtqub  16296  prmefexple  16308  bposlem1  16311  bposlem6  16316  lgslem2  16325  lgslem3  16326  lgsval  16328  lgsfcl2  16330  lgsfle1  16333  lgsle1  16339  lgsdirprm  16358  lgsne0  16362  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  gausslemma2dlem2  16386  gausslemma2dlem3  16387  gausslemma2dlem4  16388  subupgr  16719  vtxdumgrfival  16744  qdencn  17278  trilpolemlt1  17297