Metamath Proof Explorer


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 )