Theorem rspcev 2910

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 1576	. 2 ⊢ Ⅎ𝑥𝜓
2		rspcv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rspce 2905	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1397   ∈ wcel 2202  ∃wrex 2511

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-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804

This theorem is referenced by:  rspceaimv  2918  rspc2ev  2925  rspc3ev  2927  rspceeqv  2928  reu6i  2997  rspesbca  3117  brralrspcev  4147  nn0suc  4702  elrnmpt1s  4982  elrnrexdm  5786  eldmrexrn  5788  foco2  5893  elabrex  5897  elabrexg  5898  f1elima  5913  fcofo  5924  fliftfun  5936  fliftval  5940  f1oiso2  5967  fo1st  6319  fo2nd  6320  tfr0dm  6487  tfrlemisucaccv  6490  tfrlemi14d  6498  tfrexlem  6499  tfr1onlemsucaccv  6506  tfr1onlemres  6514  tfrcllemsucaccv  6519  tfrcllemres  6527  rdgss  6548  frecabcl  6564  nnaordex  6695  nnawordex  6696  ecelqsg  6756  snfig  6988  nnfi  7058  findcard  7076  fimax2gtrilemstep  7089  unsnfi  7110  eqsupti  7194  supmaxti  7202  supisoex  7207  infminti  7225  finomni  7338  nninfwlpoimlemginf  7374  isnumi  7385  oncardval  7389  archnqq  7636  prarloclemarch2  7638  prcdnql  7703  prcunqu  7704  prarloclemlo  7713  prarloclem5  7719  nqprm  7761  1idprl  7809  1idpru  7810  ltexpri  7832  prplnqu  7839  recexprlemm  7843  recexprlem1ssl  7852  recexprlem1ssu  7853  recexpr  7857  aptiprleml  7858  archpr  7862  cauappcvgprlemm  7864  cauappcvgprlemloc  7871  cauappcvgprlem1  7878  cauappcvgprlem2  7879  cauappcvgpr  7881  caucvgprlemm  7887  caucvgprlemloc  7894  caucvgprlem1  7898  caucvgprlem2  7899  caucvgpr  7901  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlem1  7928  caucvgprprlem2  7929  caucvgprpr  7931  suplocexprlemmu  7937  suplocexprlemloc  7940  suplocexpr  7944  negexsr  7991  recexgt0sr  7992  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  suplocsrlem  8027  axrnegex  8098  axprecex  8099  nntopi  8113  axcaucvglemres  8118  axpre-suploclemres  8120  cnegex  8356  recexre  8757  recexap  8832  receuap  8848  rerecapb  9022  sup3exmid  9136  cju  9140  nn2ge  9175  nominpos  9381  zdiv  9567  btwnz  9598  supinfneg  9828  infsupneg  9829  ublbneg  9846  lbzbi  9849  zq  9859  z2ge  10060  iccsupr  10200  zsupcllemstep  10488  infssuzex  10492  suprzubdc  10495  zsupssdc  10497  exbtwnzlemstep  10506  exbtwnzlemex  10508  rebtwn2zlemstep  10511  rebtwn2z  10513  qbtwnre  10515  qbtwnxr  10516  expnbnd  10924  hashunlem  11066  iswrdinn0  11117  shftlem  11376  shftfvalg  11378  shftfval  11381  caucvgre  11541  cvg1nlemres  11545  rexanuz  11548  rexuz3  11550  resqrexlemex  11585  caubnd2  11677  maxabslemval  11768  maxleast  11773  rexanre  11780  rexico  11781  fimaxre2  11787  minmax  11790  xrmaxiflemval  11810  xrmaxaddlem  11820  xrminmax  11825  climconst  11850  climshftlemg  11862  cn1lem  11874  serf0  11912  zsumdc  11944  fsum3  11947  fsum3cvg3  11956  mertenslemi1  12095  ntrivcvgap0  12109  zproddc  12139  fprodseq  12143  fprodntrivap  12144  dvdsval2  12350  dvds0lem  12361  dvds1lem  12362  dvds2lem  12363  odd2np1lem  12432  odd2np1  12433  opeo  12457  omeo  12458  divalglemex  12482  bezoutlemnewy  12566  bezoutlemaz  12573  bezoutlembz  12574  bezoutlemsup  12579  nnwodc  12606  uzwodc  12607  ncoprmgcdne1b  12660  exprmfct  12709  reumodprminv  12825  modprm0  12826  nnnn0modprm0  12827  pythagtriplem19  12854  pcprmpw2  12905  pockthi  12930  infpnlem2  12932  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemrn  13039  ennnfonelemnn0  13042  ennnfonelemim  13044  exmidunben  13046  ctinfomlemom  13047  ctinfom  13048  ctinf  13050  ctiunctlemf  13058  ismgmid2  13462  mgmidsssn0  13466  ismndd  13519  isgrpd2  13603  isgrpd  13605  imasgrp2  13696  mhmmnd  13702  ghmgrp  13704  dvdsrmuld  14109  dvdsr01  14117  rhmdvdsr  14188  lspf  14402  lspval  14403  lssats2  14427  fiinbas  14772  topbas  14790  clsval  14834  neiint  14868  neipsm  14877  opnneissb  14878  opnssneib  14879  innei  14886  restbasg  14891  lmconst  14939  iscnp4  14941  cncnpi  14951  cnconst2  14956  cnptoprest  14962  cnpdis  14965  neitx  14991  txcnp  14994  blssps  15150  blss  15151  blssexps  15152  blssex  15153  ssblex  15154  blin2  15155  neibl  15214  metss2  15221  bdmopn  15227  metrest  15229  metcnp3  15234  tgioo  15277  tgqioo  15278  addcncntoplem  15284  cnopnap  15334  dedekindeulemuub  15340  suplociccreex  15347  dedekindicclemuub  15349  ivthinclemlm  15357  ivthinclemum  15358  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthreinc  15368  elply2  15458  reeff1oleme  15495  sin0pilem2  15505  sgmnncl  15711  dvdsppwf1o  15712  perfect  15724  bj-nn0suc0  16545  bj-inf2vnlem1  16565  3dom  16587  nninfsellemeq  16616  nninfomnilem  16620  qdencn  16631  trirec0  16648