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  6529  brtposg  6530  tpostpos  6540  tposoprab  6556  th3qlem2  6917  ensn1g  7090  fndmeng  7104  xpsneng  7126  xpcomco  7130  snnen2oprc  7167  tridc  7210  fimax2gtrilemstep  7211  unsnfidcel  7234  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  9696  zlem1lt  9710  zgt0ge1  9712  qapne  10054  irrmulap  10064  divlt1lt  10141  divle1le  10142  xrltso  10214  xltnegi  10253  xltadd1  10294  xposdif  10300  xlesubadd  10301  xleaddadd  10305  nn0disj  10561  qavgle  10709  fldiv4lem1div2uz2  10761  frec2uzf1od  10863  iseqf1olemfvp  10967  seqf1oglem1  10976  exp3vallem  10997  expap0  11026  leexp2r  11050  sqap0  11063  nn0ltexp2  11168  nn0opthlem1d  11179  hashennnuni  11239  hashunlem  11265  hashf1  11308  zfz1isolemiso  11312  seq3coll  11315  swrdccatin2  11522  shftfvalg  11604  shftfibg  11606  shftfval  11607  shftfib  11609  shftfn  11610  2shfti  11617  shftidt2  11618  caucvgre  11768  cvg1nlemcau  11771  cvg1nlemres  11772  resqrexlemdecn  11799  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemsqa  11811  resqrexlemex  11812  abs00ap  11849  absdiflt  11880  absdifle  11881  lenegsq  11883  cau3lem  11902  fiidxsupcl  12017  minmax  12019  xrmaxltsup  12048  xrminmax  12055  xrltmininf  12060  xrlemininf  12061  clim  12071  clim2  12073  clim0  12075  clim0c  12076  climi0  12079  climuni  12083  2clim  12091  climshftlemg  12092  climshft  12094  climabs0  12097  climcn1  12098  climcn2  12099  addcn2  12100  subcn2  12101  mulcn2  12102  iser3shft  12136  climcau  12137  serf0  12142  sumeq1  12145  sumeq2  12149  sumrbdc  12170  summodclem2  12173  summodc  12174  zsumdc  12175  isumshft  12281  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  prodfap0  12336  prodfrecap  12337  prodfdivap  12338  ntrivcvgap  12339  ntrivcvgap0  12340  prodeq1f  12343  prodeq2w  12347  prodeq2  12348  prodrbdclem2  12364  prodmodclem2  12368  prodmodc  12369  zproddc  12370  fprodntrivap  12375  fprodap0  12412  fprodrec  12420  fproddivapf  12422  fprodap0f  12427  tanaddaplem  12529  sin01bnd  12548  cos01bnd  12549  halfleoddlt  12685  gcddvds  12764  dvdssq  12832  lcmgcdlem  12879  lcmdvds  12881  isprm  12911  prmgt1  12935  isprm5lem  12944  isprm6  12950  pwbdvdslemn  12968  pwbdvdseu  12971  nnmaxpwlemxy  12972  nnmaxpwlemnfac  12975  sqrtrirr  13013  odzdvds  13052  pclem0  13093  pclemub  13094  pclemdc  13095  pcprecl  13096  pcprendvds  13097  pcpremul  13100  pceulem  13101  pcval  13103  pcelnn  13128  pc2dvds  13137  pcadd  13147  pcadd2  13148  pcmpt  13150  prmpwdvds  13162  4sqlem17  13214  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemodife  13297  ballotfilemic  13307  ballotfilemsv  13310  ballotfilemrc  13331  imasaddfnlemg  13693  znf1o  15094  znidomb  15101  psrbaglefifi  15175  psrbagmaxlem1  15178  psrbagmax  15183  blfvalps  15628  elblps  15633  elbl  15634  elbl3ps  15637  elbl3  15638  blres  15677  comet  15742  bdbl  15746  xmetxp  15750  xmetxpbl  15751  metcnp2  15756  txmetcnp  15761  cnbl0  15777  cnblcld  15778  bl2ioo  15793  addcncntoplem  15804  divcnap  15808  mpomulcn  15809  elcncf  15816  elcncf2  15817  cncfi  15821  rescncf  15824  mulc1cncf  15832  cncfco  15834  cncfmet  15835  cncfmptid  15840  addccncf  15843  cdivcncfap  15847  negcncf  15848  mulcncflem  15850  mulcncf  15851  ivthinclemlm  15877  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemdisj  15883  ivthinclemloc  15884  ivthinc  15886  ivthreinc  15888  limccl  15902  ellimc3apf  15903  limcdifap  15905  limcmpted  15906  limcimolemlt  15907  limcresi  15909  cnplimcim  15910  limccnpcntop  15918  limccnp2lem  15919  limccoap  15921  dvcoapbr  15950  dveflem  15969  eflt  16018  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  logltb  16121  logge0b  16137  loggt0b  16138  zprmlogbaplem2  16233  zprmlogbap  16235  pellexlem3  16248  chtublem  16312  chtqub  16313  prmefexple  16325  bposlem1  16328  bposlem6  16333  lgslem2  16342  lgslem3  16343  lgsval  16345  lgsfcl2  16347  lgsfle1  16350  lgsle1  16356  lgsdirprm  16375  lgsne0  16379  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  gausslemma2dlem2  16403  gausslemma2dlem3  16404  gausslemma2dlem4  16405  subupgr  16736  vtxdumgrfival  16761  qdencn  17295  trilpolemlt1  17314