Step |
Hyp |
Ref |
Expression |
1 |
|
bj-elabd2ALT.ex |
|- ( ph -> A e. V ) |
2 |
|
bj-elabd2ALT.eq |
|- ( ph -> B = { x | ps } ) |
3 |
|
bj-elabd2ALT.is |
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) |
4 |
|
simpr |
|- ( ( ph /\ y = A ) -> y = A ) |
5 |
2
|
eqcomd |
|- ( ph -> { x | ps } = B ) |
6 |
5
|
adantr |
|- ( ( ph /\ y = A ) -> { x | ps } = B ) |
7 |
4 6
|
eleq12d |
|- ( ( ph /\ y = A ) -> ( y e. { x | ps } <-> A e. B ) ) |
8 |
|
eqeq1 |
|- ( x = y -> ( x = A <-> y = A ) ) |
9 |
8
|
biimparc |
|- ( ( y = A /\ x = y ) -> x = A ) |
10 |
9
|
anim2i |
|- ( ( ph /\ ( y = A /\ x = y ) ) -> ( ph /\ x = A ) ) |
11 |
10
|
anassrs |
|- ( ( ( ph /\ y = A ) /\ x = y ) -> ( ph /\ x = A ) ) |
12 |
11 3
|
syl |
|- ( ( ( ph /\ y = A ) /\ x = y ) -> ( ps <-> ch ) ) |
13 |
12
|
sbiedvw |
|- ( ( ph /\ y = A ) -> ( [ y / x ] ps <-> ch ) ) |
14 |
7 13
|
bibi12d |
|- ( ( ph /\ y = A ) -> ( ( y e. { x | ps } <-> [ y / x ] ps ) <-> ( A e. B <-> ch ) ) ) |
15 |
|
df-clab |
|- ( y e. { x | ps } <-> [ y / x ] ps ) |
16 |
15
|
a1i |
|- ( ph -> ( y e. { x | ps } <-> [ y / x ] ps ) ) |
17 |
1 14 16
|
vtocld |
|- ( ph -> ( A e. B <-> ch ) ) |