Theorem rspcev 2656

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

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1243   ∈ wcel 1393  ∃wrex 2307

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559

This theorem is referenced by:  rspc2ev  2664  rspc3ev  2666  reu6i  2732  rspesbca  2842  nn0suc  4327  elrnmpt1s  4584  elrnrexdm  5306  eldmrexrn  5308  foco2  5318  elabrex  5397  f1elima  5412  fcofo  5424  fliftfun  5436  fliftval  5440  f1oiso2  5466  fo1st  5784  fo2nd  5785  tfr0  5937  tfrlemisucaccv  5939  tfrlemi14d  5947  tfrexlem  5948  rdgss  5970  nnaordex  6100  nnawordex  6101  ecelqsg  6159  snfig  6291  nnfi  6333  findcard  6345  isnumi  6362  oncardval  6366  archnqq  6515  prarloclemarch2  6517  prcdnql  6582  prcunqu  6583  prarloclemlo  6592  prarloclem5  6598  nqprm  6640  1idprl  6688  1idpru  6689  ltexpri  6711  prplnqu  6718  recexprlemm  6722  recexprlem1ssl  6731  recexprlem1ssu  6732  recexpr  6736  aptiprleml  6737  archpr  6741  cauappcvgprlemm  6743  cauappcvgprlemloc  6750  cauappcvgprlem1  6757  cauappcvgprlem2  6758  cauappcvgpr  6760  caucvgprlemm  6766  caucvgprlemloc  6773  caucvgprlem1  6777  caucvgprlem2  6778  caucvgpr  6780  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlem1  6807  caucvgprprlem2  6808  caucvgprpr  6810  negexsr  6857  recexgt0sr  6858  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  axrnegex  6953  axprecex  6954  nntopi  6968  axcaucvglemres  6973  cnegex  7189  recexre  7569  recexap  7634  receuap  7650  cju  7913  nn2ge  7946  nominpos  8162  zdiv  8328  btwnz  8357  ublbneg  8548  lbzbi  8551  zq  8561  z2ge  8739  iccsupr  8835  qbtwnzlemstep  9103  qbtwnzlemex  9105  rebtwn2zlemstep  9107  rebtwn2z  9109  qbtwnre  9111  expnbnd  9372  shftlem  9417  shftfvalg  9419  shftfval  9422  caucvgre  9580  cvg1nlemres  9584  rexanuz  9587  rexuz3  9588  resqrexlemex  9623  caubnd2  9713  climconst  9811  climshftlemg  9823  cn1lem  9834  serif0  9871  bj-nn0suc0  10075  bj-inf2vnlem1  10095  qdencn  10124