Theorem rspcev 2839

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcev	⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcev

Step	Hyp	Ref	Expression
1		nfv 1526	. 2 ⊢ Ⅎ𝑥𝜓
2		rspcv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rspce 2834	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2146  ∃wrex 2454

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-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-v 2737

This theorem is referenced by:  rspceaimv  2847  rspc2ev  2854  rspc3ev  2856  rspceeqv  2857  reu6i  2926  rspesbca  3045  brralrspcev  4056  nn0suc  4597  elrnmpt1s  4870  elrnrexdm  5647  eldmrexrn  5649  foco2  5745  elabrex  5749  f1elima  5764  fcofo  5775  fliftfun  5787  fliftval  5791  f1oiso2  5818  fo1st  6148  fo2nd  6149  tfr0dm  6313  tfrlemisucaccv  6316  tfrlemi14d  6324  tfrexlem  6325  tfr1onlemsucaccv  6332  tfr1onlemres  6340  tfrcllemsucaccv  6345  tfrcllemres  6353  rdgss  6374  frecabcl  6390  nnaordex  6519  nnawordex  6520  ecelqsg  6578  snfig  6804  nnfi  6862  findcard  6878  fimax2gtrilemstep  6890  unsnfi  6908  eqsupti  6985  supmaxti  6993  supisoex  6998  infminti  7016  finomni  7128  nninfwlpoimlemginf  7164  isnumi  7171  oncardval  7175  archnqq  7391  prarloclemarch2  7393  prcdnql  7458  prcunqu  7459  prarloclemlo  7468  prarloclem5  7474  nqprm  7516  1idprl  7564  1idpru  7565  ltexpri  7587  prplnqu  7594  recexprlemm  7598  recexprlem1ssl  7607  recexprlem1ssu  7608  recexpr  7612  aptiprleml  7613  archpr  7617  cauappcvgprlemm  7619  cauappcvgprlemloc  7626  cauappcvgprlem1  7633  cauappcvgprlem2  7634  cauappcvgpr  7636  caucvgprlemm  7642  caucvgprlemloc  7649  caucvgprlem1  7653  caucvgprlem2  7654  caucvgpr  7656  caucvgprprlemmu  7669  caucvgprprlemopl  7671  caucvgprprlemopu  7673  caucvgprprlemloc  7677  caucvgprprlem1  7683  caucvgprprlem2  7684  caucvgprpr  7686  suplocexprlemmu  7692  suplocexprlemloc  7695  suplocexpr  7699  negexsr  7746  recexgt0sr  7747  caucvgsrlemgt1  7769  caucvgsrlemoffres  7774  suplocsrlem  7782  axrnegex  7853  axprecex  7854  nntopi  7868  axcaucvglemres  7873  axpre-suploclemres  7875  cnegex  8109  recexre  8509  recexap  8583  receuap  8599  sup3exmid  8885  cju  8889  nn2ge  8923  nominpos  9127  zdiv  9312  btwnz  9343  supinfneg  9566  infsupneg  9567  ublbneg  9584  lbzbi  9587  zq  9597  z2ge  9795  iccsupr  9935  exbtwnzlemstep  10216  exbtwnzlemex  10218  rebtwn2zlemstep  10221  rebtwn2z  10223  qbtwnre  10225  qbtwnxr  10226  expnbnd  10611  hashunlem  10750  shftlem  10791  shftfvalg  10793  shftfval  10796  caucvgre  10956  cvg1nlemres  10960  rexanuz  10963  rexuz3  10965  resqrexlemex  11000  caubnd2  11092  maxabslemval  11183  maxleast  11188  rexanre  11195  rexico  11196  fimaxre2  11201  minmax  11204  xrmaxiflemval  11224  xrmaxaddlem  11234  xrminmax  11239  climconst  11264  climshftlemg  11276  cn1lem  11288  serf0  11326  zsumdc  11358  fsum3  11361  fsum3cvg3  11370  mertenslemi1  11509  ntrivcvgap0  11523  zproddc  11553  fprodseq  11557  fprodntrivap  11558  dvdsval2  11763  dvds0lem  11774  dvds1lem  11775  dvds2lem  11776  odd2np1lem  11842  odd2np1  11843  opeo  11867  omeo  11868  divalglemex  11892  zsupcllemstep  11911  infssuzex  11915  suprzubdc  11918  zsupssdc  11920  bezoutlemnewy  11962  bezoutlemaz  11969  bezoutlembz  11970  bezoutlemsup  11975  nnwodc  12002  uzwodc  12003  ncoprmgcdne1b  12054  exprmfct  12103  reumodprminv  12218  modprm0  12219  nnnn0modprm0  12220  pythagtriplem19  12247  pcprmpw2  12297  pockthi  12321  infpnlem2  12323  ennnfonelemex  12380  ennnfonelemhom  12381  ennnfonelemrn  12385  ennnfonelemnn0  12388  ennnfonelemim  12390  exmidunben  12392  ctinfomlemom  12393  ctinfom  12394  ctinf  12396  ctiunctlemf  12404  ismgmid2  12663  mgmidsssn0  12667  ismndd  12702  isgrpd2  12757  isgrpd  12759  mhmmnd  12839  ghmgrp  12841  fiinbas  13116  topbas  13136  clsval  13180  neiint  13214  neipsm  13223  opnneissb  13224  opnssneib  13225  innei  13232  restbasg  13237  lmconst  13285  iscnp4  13287  cncnpi  13297  cnconst2  13302  cnptoprest  13308  cnpdis  13311  neitx  13337  txcnp  13340  blssps  13496  blss  13497  blssexps  13498  blssex  13499  ssblex  13500  blin2  13501  neibl  13560  metss2  13567  bdmopn  13573  metrest  13575  metcnp3  13580  tgioo  13615  tgqioo  13616  addcncntoplem  13620  cnopnap  13663  dedekindeulemuub  13664  suplociccreex  13671  dedekindicclemuub  13673  ivthinclemlm  13681  ivthinclemum  13682  ivthinclemlopn  13683  ivthinclemuopn  13685  reeff1oleme  13762  sin0pilem2  13772  bj-nn0suc0  14260  bj-inf2vnlem1  14280  nninfsellemeq  14322  nninfomnilem  14326  qdencn  14334  trirec0  14351