Step |
Hyp |
Ref |
Expression |
1 |
|
abfmpel.1 |
|- F = ( x e. V |-> { y | ph } ) |
2 |
|
abfmpel.2 |
|- { y | ph } e. _V |
3 |
|
abfmpel.3 |
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) |
4 |
2
|
csbex |
|- [_ A / x ]_ { y | ph } e. _V |
5 |
1
|
fvmpts |
|- ( ( A e. V /\ [_ A / x ]_ { y | ph } e. _V ) -> ( F ` A ) = [_ A / x ]_ { y | ph } ) |
6 |
4 5
|
mpan2 |
|- ( A e. V -> ( F ` A ) = [_ A / x ]_ { y | ph } ) |
7 |
|
csbab |
|- [_ A / x ]_ { y | ph } = { y | [. A / x ]. ph } |
8 |
6 7
|
eqtrdi |
|- ( A e. V -> ( F ` A ) = { y | [. A / x ]. ph } ) |
9 |
8
|
eleq2d |
|- ( A e. V -> ( B e. ( F ` A ) <-> B e. { y | [. A / x ]. ph } ) ) |
10 |
9
|
adantr |
|- ( ( A e. V /\ B e. W ) -> ( B e. ( F ` A ) <-> B e. { y | [. A / x ]. ph } ) ) |
11 |
|
simpl |
|- ( ( A e. V /\ y = B ) -> A e. V ) |
12 |
3
|
ancoms |
|- ( ( y = B /\ x = A ) -> ( ph <-> ps ) ) |
13 |
12
|
adantll |
|- ( ( ( A e. V /\ y = B ) /\ x = A ) -> ( ph <-> ps ) ) |
14 |
11 13
|
sbcied |
|- ( ( A e. V /\ y = B ) -> ( [. A / x ]. ph <-> ps ) ) |
15 |
14
|
ex |
|- ( A e. V -> ( y = B -> ( [. A / x ]. ph <-> ps ) ) ) |
16 |
15
|
alrimiv |
|- ( A e. V -> A. y ( y = B -> ( [. A / x ]. ph <-> ps ) ) ) |
17 |
|
elabgt |
|- ( ( B e. W /\ A. y ( y = B -> ( [. A / x ]. ph <-> ps ) ) ) -> ( B e. { y | [. A / x ]. ph } <-> ps ) ) |
18 |
16 17
|
sylan2 |
|- ( ( B e. W /\ A e. V ) -> ( B e. { y | [. A / x ]. ph } <-> ps ) ) |
19 |
18
|
ancoms |
|- ( ( A e. V /\ B e. W ) -> ( B e. { y | [. A / x ]. ph } <-> ps ) ) |
20 |
10 19
|
bitrd |
|- ( ( A e. V /\ B e. W ) -> ( B e. ( F ` A ) <-> ps ) ) |