Theorem abrexex2g 7962

Description: Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)

Assertion

Ref	Expression
abrexex2g	⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝑉,𝑦   𝑥,𝑊,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem abrexex2g

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1944	. . . 4 ⊢ Ⅎ𝑧∃𝑥 ∈ 𝐴 𝜑
2		nfcv 2925	. . . . 5 ⊢ Ⅎ𝑦𝐴
3		nfs1v 2191	. . . . 5 ⊢ Ⅎ𝑦[𝑧 / 𝑦]𝜑
4	2, 3	nfrexw 3313	. . . 4 ⊢ Ⅎ𝑦∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑
5		sbequ12 2287	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑦]𝜑))
6	5	rexbidv 3189	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑))
7	1, 4, 6	cbvabw 2834	. . 3 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑}
8		df-clab 2742	. . . . 5 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} ↔ [𝑧 / 𝑦]𝜑)
9	8	rexbii 3112	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ {𝑦 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑)
10	9	abbii 2830	. . 3 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ {𝑦 ∣ 𝜑}} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑}
11	7, 10	eqtr4i 2789	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ {𝑦 ∣ 𝜑}}
12		df-iun 4959	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ {𝑦 ∣ 𝜑}}
13		iunexg 7961	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ V)
14	12, 13	eqeltrrid 2868	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ {𝑦 ∣ 𝜑}} ∈ V)
15	11, 14	eqeltrid 2867	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V)

Syntax hints:   → wi 4   ∧ wa 400  [wsb 2096   ∈ wcel 2143  {cab 2741  ∀wral 3079  ∃wrex 3089  Vcvv 3455  ∪ ciun 4957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-v 3457  df-ss 3923  df-uni 4874  df-iun 4959

This theorem is referenced by:  abrexex2  7967  ptrescn  23777  satfvsuclem1  35829  satf0suclem  35845  fmlasuc0  35854  sdclem2  38371  sdclem1  38372  sprval  48205  prprval  48240