Theorem rspcev 2955

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

Hypothesis

Ref	Expression
rspcv.1	⊢ (x = A → (φ ↔ ψ))

Assertion

Ref	Expression
rspcev	⊢ ((A ∈ B ∧ ψ) → ∃x ∈ B φ)

Distinct variable groups:   x,A   x,B   ψ,x

Allowed substitution hint:   φ(x)

Proof of Theorem rspcev

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxψ
2		rspcv.1	. 2 ⊢ (x = A → (φ ↔ ψ))
3	1, 2	rspce 2950	1 ⊢ ((A ∈ B ∧ ψ) → ∃x ∈ B φ)

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642   ∈ wcel 1710  ∃wrex 2615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-rex 2620  df-v 2861

This theorem is referenced by:  rspc2ev  2963  rspc3ev  2965  reu6i  3027  rspesbca  3126  pwadjoin  4119  eqpw1uni  4330  nnc0suc  4412  elsuci  4414  0fin  4423  nnsucelr  4428  snfi  4431  lefinaddc  4450  nulge  4456  leltfintr  4458  ltfintr  4459  ltfinp1  4462  lefinlteq  4463  lefinrflx  4467  ltlefin  4468  ssfin  4470  ncfinraise  4481  ncfinlower  4483  tfinltfinlem1  4500  0ceven  4505  sucoddeven  4511  eventfin  4517  oddtfin  4518  nnpweq  4523  vfinspss  4551  phi11lem1  4595  foco2  5426  f1elima  5474  f1oiso2  5500  clos1conn  5879  clos1basesuc  5882  ecelqsg  5979  ncspw1eu  6159  pw1eltc  6162  nntccl  6170  lecidg  6196  lecncvg  6199  dflec2  6210  dflec3  6221  lenc  6223  letc  6231  ce0t  6232  ce0lenc1  6239  ncfin  6247  nmembers1lem3  6270  nncdiv3  6277  nchoicelem13  6301  nchoicelem17  6305  nchoicelem19  6307  nchoice  6308  frecsuc  6322