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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fabexg.1 | ||
2 | elex | ||
3 | elex | ||
4 | simprl | ||
5 | simpl | ||
6 | simpr | ||
7 | 4 5 6 | fabexd | |
8 | 1 7 | eqeltrid | |
9 | 2 3 8 | syl2an |