Theorem rspce 3594

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.)

Hypotheses

Ref	Expression
rspc.1	⊢ Ⅎ𝑥𝜓
rspc.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rspce

Step	Hyp	Ref	Expression
1		nfcv 2897	. . . 4 ⊢ Ⅎ𝑥𝐴
2		nfv 1913	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
3		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfan 1898	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓)
5		eleq1 2821	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
8	1, 4, 7	spcegf 3575	. . 3 ⊢ (𝐴 ∈ 𝐵 → ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
9	8	anabsi5 669	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
10		df-rex 3060	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
11	9, 10	sylibr 234	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539  ∃wex 1778  Ⅎwnf 1782   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-cleq 2726  df-clel 2808  df-nfc 2884  df-rex 3060

This theorem is referenced by:  reuop  6293  ac6c4  10503  infcvgaux1i  15875  iunmbl2  25528  gsumpart  32999  esumcvg  34046  ptrecube  37586  poimirlem24  37610  sdclem1  37709  uzwo4  45015  eliuniincex  45071  elrnmpt1sf  45151  iuneqfzuzlem  45302  uzublem  45398  uzub  45399  limsupubuzlem  45684  sge0gerp  46367  smflim  46749  reupr  47467