Step |
Hyp |
Ref |
Expression |
1 |
|
vtocl2.1 |
|- A e. _V |
2 |
|
vtocl2.2 |
|- B e. _V |
3 |
|
vtocl2.3 |
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) |
4 |
|
vtocl2.4 |
|- ph |
5 |
1
|
isseti |
|- E. x x = A |
6 |
2
|
isseti |
|- E. y y = B |
7 |
|
exdistrv |
|- ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) ) |
8 |
3
|
biimpd |
|- ( ( x = A /\ y = B ) -> ( ph -> ps ) ) |
9 |
8
|
2eximi |
|- ( E. x E. y ( x = A /\ y = B ) -> E. x E. y ( ph -> ps ) ) |
10 |
7 9
|
sylbir |
|- ( ( E. x x = A /\ E. y y = B ) -> E. x E. y ( ph -> ps ) ) |
11 |
5 6 10
|
mp2an |
|- E. x E. y ( ph -> ps ) |
12 |
|
19.36v |
|- ( E. y ( ph -> ps ) <-> ( A. y ph -> ps ) ) |
13 |
12
|
exbii |
|- ( E. x E. y ( ph -> ps ) <-> E. x ( A. y ph -> ps ) ) |
14 |
11 13
|
mpbi |
|- E. x ( A. y ph -> ps ) |
15 |
14
|
19.36iv |
|- ( A. x A. y ph -> ps ) |
16 |
4
|
ax-gen |
|- A. y ph |
17 |
15 16
|
mpg |
|- ps |