Step |
Hyp |
Ref |
Expression |
1 |
|
riotasv2d.1 |
|- F/ y ph |
2 |
|
riotasv2d.2 |
|- ( ph -> F/_ y F ) |
3 |
|
riotasv2d.3 |
|- ( ph -> F/ y ch ) |
4 |
|
riotasv2d.4 |
|- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) ) |
5 |
|
riotasv2d.5 |
|- ( ( ph /\ y = E ) -> ( ps <-> ch ) ) |
6 |
|
riotasv2d.6 |
|- ( ( ph /\ y = E ) -> C = F ) |
7 |
|
riotasv2d.7 |
|- ( ph -> D e. A ) |
8 |
|
riotasv2d.8 |
|- ( ph -> E e. B ) |
9 |
|
riotasv2d.9 |
|- ( ph -> ch ) |
10 |
|
elex |
|- ( A e. V -> A e. _V ) |
11 |
8
|
adantr |
|- ( ( ph /\ A e. _V ) -> E e. B ) |
12 |
9
|
adantr |
|- ( ( ph /\ A e. _V ) -> ch ) |
13 |
|
eleq1 |
|- ( y = E -> ( y e. B <-> E e. B ) ) |
14 |
13
|
adantl |
|- ( ( ph /\ y = E ) -> ( y e. B <-> E e. B ) ) |
15 |
14 5
|
anbi12d |
|- ( ( ph /\ y = E ) -> ( ( y e. B /\ ps ) <-> ( E e. B /\ ch ) ) ) |
16 |
6
|
eqeq2d |
|- ( ( ph /\ y = E ) -> ( D = C <-> D = F ) ) |
17 |
15 16
|
imbi12d |
|- ( ( ph /\ y = E ) -> ( ( ( y e. B /\ ps ) -> D = C ) <-> ( ( E e. B /\ ch ) -> D = F ) ) ) |
18 |
17
|
adantlr |
|- ( ( ( ph /\ A e. _V ) /\ y = E ) -> ( ( ( y e. B /\ ps ) -> D = C ) <-> ( ( E e. B /\ ch ) -> D = F ) ) ) |
19 |
4 7
|
riotasvd |
|- ( ( ph /\ A e. _V ) -> ( ( y e. B /\ ps ) -> D = C ) ) |
20 |
|
nfv |
|- F/ y A e. _V |
21 |
1 20
|
nfan |
|- F/ y ( ph /\ A e. _V ) |
22 |
|
nfcvd |
|- ( ( ph /\ A e. _V ) -> F/_ y E ) |
23 |
|
nfvd |
|- ( ph -> F/ y E e. B ) |
24 |
23 3
|
nfand |
|- ( ph -> F/ y ( E e. B /\ ch ) ) |
25 |
|
nfra1 |
|- F/ y A. y e. B ( ps -> x = C ) |
26 |
|
nfcv |
|- F/_ y A |
27 |
25 26
|
nfriota |
|- F/_ y ( iota_ x e. A A. y e. B ( ps -> x = C ) ) |
28 |
1 4
|
nfceqdf |
|- ( ph -> ( F/_ y D <-> F/_ y ( iota_ x e. A A. y e. B ( ps -> x = C ) ) ) ) |
29 |
27 28
|
mpbiri |
|- ( ph -> F/_ y D ) |
30 |
29 2
|
nfeqd |
|- ( ph -> F/ y D = F ) |
31 |
24 30
|
nfimd |
|- ( ph -> F/ y ( ( E e. B /\ ch ) -> D = F ) ) |
32 |
31
|
adantr |
|- ( ( ph /\ A e. _V ) -> F/ y ( ( E e. B /\ ch ) -> D = F ) ) |
33 |
11 18 19 21 22 32
|
vtocldf |
|- ( ( ph /\ A e. _V ) -> ( ( E e. B /\ ch ) -> D = F ) ) |
34 |
11 12 33
|
mp2and |
|- ( ( ph /\ A e. _V ) -> D = F ) |
35 |
10 34
|
sylan2 |
|- ( ( ph /\ A e. V ) -> D = F ) |