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 1947	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
3		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfan 1932	. . . 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 1570  ∃wex 1812  Ⅎwnf 1816   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

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

This theorem is used by:  reuop  6291  ac6c4  10483  infcvgaux1i  15946  iunmbl2  25785  gsumpart  33503  esumcvg  34596  ptrecube  38369  poimirlem24  38393  sdclem1  38493  uzwo4  45887  eliuniincex  45941  elrnmpt1sf  46021  iuneqfzuzlem  46164  uzublem  46258  uzub  46259  limsupubuzlem  46540  sge0gerp  47223  smflim  47605  reupr  48422