Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
|- m e. _V |
2 |
|
feq1 |
|- ( f = m -> ( f : A --> B <-> m : A --> B ) ) |
3 |
1 2
|
elab |
|- ( m e. { f | f : A --> B } <-> m : A --> B ) |
4 |
|
simpr |
|- ( ( m : A --> B /\ B e. V ) -> B e. V ) |
5 |
|
dmfex |
|- ( ( m e. _V /\ m : A --> B ) -> A e. _V ) |
6 |
1 5
|
mpan |
|- ( m : A --> B -> A e. _V ) |
7 |
6
|
adantr |
|- ( ( m : A --> B /\ B e. V ) -> A e. _V ) |
8 |
4 7
|
elmapd |
|- ( ( m : A --> B /\ B e. V ) -> ( m e. ( B ^m A ) <-> m : A --> B ) ) |
9 |
8
|
exbiri |
|- ( m : A --> B -> ( B e. V -> ( m : A --> B -> m e. ( B ^m A ) ) ) ) |
10 |
9
|
pm2.43b |
|- ( B e. V -> ( m : A --> B -> m e. ( B ^m A ) ) ) |
11 |
|
elmapi |
|- ( m e. ( B ^m A ) -> m : A --> B ) |
12 |
10 11
|
impbid1 |
|- ( B e. V -> ( m : A --> B <-> m e. ( B ^m A ) ) ) |
13 |
3 12
|
bitrid |
|- ( B e. V -> ( m e. { f | f : A --> B } <-> m e. ( B ^m A ) ) ) |
14 |
13
|
eqrdv |
|- ( B e. V -> { f | f : A --> B } = ( B ^m A ) ) |