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 ⊢ F = x | x : A ⟶ B ∧ φ
Assertion fabexg ⊢ A ∈ C ∧ B ∈ D → F ∈ V

Proof

Step Hyp Ref Expression
1 fabexg.1 ⊢ F = x | x : A ⟶ B ∧ φ
2 elex ⊢ A ∈ C → A ∈ V
3 elex ⊢ B ∈ D → B ∈ V
4 simprl ⊢ A ∈ V ∧ B ∈ V ∧ x : A ⟶ B ∧ φ → x : A ⟶ B
5 simpl ⊢ A ∈ V ∧ B ∈ V → A ∈ V
6 simpr ⊢ A ∈ V ∧ B ∈ V → B ∈ V
7 4 5 6 fabexd ⊢ A ∈ V ∧ B ∈ V → x | x : A ⟶ B ∧ φ ∈ V
8 1 7 eqeltrid ⊢ A ∈ V ∧ B ∈ V → F ∈ V
9 2 3 8 syl2an ⊢ A ∈ C ∧ B ∈ D → F ∈ V