Theorem rspce 3565

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 2922	. . . 4 ⊢ Ⅎ𝑥𝐴
2		nfv 1946	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
3		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfan 1931	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓)
5		eleq1 2848	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	anbi12d 644	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
8	1, 4, 7	spcegf 3546	. . 3 ⊢ (𝐴 ∈ 𝐵 → ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
9	8	anabsi5 682	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
10		df-rex 3087	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
11	9, 10	sylibr 237	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811  Ⅎwnf 1815   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rex 3087

This theorem is used by:  reuop  6299  ac6c4  10566  infcvgaux1i  16035  iunmbl2  25887  gsumpart  33674  esumcvg  34768  ptrecube  38647  poimirlem24  38671  sdclem1  38786  uzwo4  46178  eliuniincex  46232  elrnmpt1sf  46312  iuneqfzuzlem  46454  uzublem  46548  uzub  46549  limsupubuzlem  46830  sge0gerp  47513  smflim  47895  reupr  48712