Theorem rspce 3609

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 2976	. . . 4 ⊢ Ⅎ𝑥𝐴
2		nfv 1914	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
3		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfan 1899	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓)
5		eleq1 2899	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
8	1, 4, 7	spcegf 3588	. . 3 ⊢ (𝐴 ∈ 𝐵 → ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
9	8	anabsi5 667	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
10		df-rex 3143	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
11	9, 10	sylibr 236	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536  ∃wex 1779  Ⅎwnf 1783   ∈ wcel 2113  ∃wrex 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-rex 3143  df-v 3493

This theorem is referenced by:  rspcevOLD  3621  reuop  6137  ac6c4  9896  infcvgaux1i  15207  iunmbl2  24153  esumcvg  31366  ptrecube  34927  poimirlem24  34951  sdclem1  35051  uzwo4  41389  eliuniincex  41449  elrnmpt1sf  41524  iuneqfzuzlem  41676  uzublem  41778  uzub  41779  limsupubuzlem  42067  sge0gerp  42751  smflim  43127  reupr  43758