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