Theorem fabexg

Description: Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008)

	Ref	Expression
Hypothesis	fabexg.1	⊢ 𝐹 = { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) }
Assertion	fabexg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		fabexg.1	⊢ 𝐹 = { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) }
2		xpexg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 × 𝐵 ) ∈ V )
3		pwexg	⊢ ( ( 𝐴 × 𝐵 ) ∈ V → 𝒫 ( 𝐴 × 𝐵 ) ∈ V )
4		fssxp	⊢ ( 𝑥 : 𝐴 ⟶ 𝐵 → 𝑥 ⊆ ( 𝐴 × 𝐵 ) )
5		velpw	⊢ ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↔ 𝑥 ⊆ ( 𝐴 × 𝐵 ) )
6	4 5	sylibr	⊢ ( 𝑥 : 𝐴 ⟶ 𝐵 → 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) )
7	6	anim1i	⊢ ( ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝜑 ) )
8	7	ss2abi	⊢ { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝜑 ) }
9	1 8	eqsstri	⊢ 𝐹 ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝜑 ) }
10		ssab2	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } ⊆ 𝒫 ( 𝐴 × 𝐵 )
11	9 10	sstri	⊢ 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐵 )
12		ssexg	⊢ ( ( 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝒫 ( 𝐴 × 𝐵 ) ∈ V ) → 𝐹 ∈ V )
13	11 12	mpan	⊢ ( 𝒫 ( 𝐴 × 𝐵 ) ∈ V → 𝐹 ∈ V )
14	2 3 13	3syl	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V )