Theorem rspcev 2956

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 2951	1 ⊢ ((A ∈ B ∧ ψ) → ∃x ∈ B φ)

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

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 2479  df-rex 2621  df-v 2862

This theorem is referenced by:  rspc2ev  2964  rspc3ev  2966  reu6i  3028  rspesbca  3127  pwadjoin  4120  eqpw1uni  4331  nnc0suc  4413  elsuci  4415  0fin  4424  nnsucelr  4429  snfi  4432  lefinaddc  4451  nulge  4457  leltfintr  4459  ltfintr  4460  ltfinp1  4463  lefinlteq  4464  lefinrflx  4468  ltlefin  4469  ssfin  4471  ncfinraise  4482  ncfinlower  4484  tfinltfinlem1  4501  0ceven  4506  sucoddeven  4512  eventfin  4518  oddtfin  4519  nnpweq  4524  vfinspss  4552  phi11lem1  4596  foco2  5427  f1elima  5475  f1oiso2  5501  clos1conn  5880  clos1basesuc  5883  ecelqsg  5980  ncspw1eu  6160  pw1eltc  6163  nntccl  6171  lecidg  6197  lecncvg  6200  dflec2  6211  dflec3  6222  lenc  6224  letc  6232  ce0t  6233  ce0lenc1  6240  ncfin  6248  nmembers1lem3  6271  nncdiv3  6278  nchoicelem13  6302  nchoicelem17  6306  nchoicelem19  6308  nchoice  6309  frecsuc  6323