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