Theorem fabexg

Description: Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008) (Proof shortened by AV, 9-Jun-2025)

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

Proof

Step	Hyp	Ref	Expression
1		fabexg.1	⊢ 𝐹 = { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) }
2		elex	⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ V )
3		elex	⊢ ( 𝐵 ∈ 𝐷 → 𝐵 ∈ V )
4		simprl	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) ) → 𝑥 : 𝐴 ⟶ 𝐵 )
5		simpl	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
6		simpr	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
7	4 5 6	fabexd	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) } ∈ V )
8	1 7	eqeltrid	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐹 ∈ V )
9	2 3 8	syl2an	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V )