Step |
Hyp |
Ref |
Expression |
1 |
|
fabexg.1 |
|- F = { x | ( x : A --> B /\ ph ) } |
2 |
|
elex |
|- ( A e. C -> A e. _V ) |
3 |
|
elex |
|- ( B e. D -> B e. _V ) |
4 |
|
simprl |
|- ( ( ( A e. _V /\ B e. _V ) /\ ( x : A --> B /\ ph ) ) -> x : A --> B ) |
5 |
|
simpl |
|- ( ( A e. _V /\ B e. _V ) -> A e. _V ) |
6 |
|
simpr |
|- ( ( A e. _V /\ B e. _V ) -> B e. _V ) |
7 |
4 5 6
|
fabexd |
|- ( ( A e. _V /\ B e. _V ) -> { x | ( x : A --> B /\ ph ) } e. _V ) |
8 |
1 7
|
eqeltrid |
|- ( ( A e. _V /\ B e. _V ) -> F e. _V ) |
9 |
2 3 8
|
syl2an |
|- ( ( A e. C /\ B e. D ) -> F e. _V ) |