Step |
Hyp |
Ref |
Expression |
1 |
|
riotasv2s.2 |
|- D = ( iota_ x e. A A. y e. B ( ph -> x = C ) ) |
2 |
|
3simpc |
|- ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) ) |
3 |
|
simp1 |
|- ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> A e. V ) |
4 |
|
nfra1 |
|- F/ y A. y e. B ( ph -> x = C ) |
5 |
|
nfcv |
|- F/_ y A |
6 |
4 5
|
nfriota |
|- F/_ y ( iota_ x e. A A. y e. B ( ph -> x = C ) ) |
7 |
1 6
|
nfcxfr |
|- F/_ y D |
8 |
7
|
nfel1 |
|- F/ y D e. A |
9 |
|
nfv |
|- F/ y E e. B |
10 |
|
nfsbc1v |
|- F/ y [. E / y ]. ph |
11 |
9 10
|
nfan |
|- F/ y ( E e. B /\ [. E / y ]. ph ) |
12 |
8 11
|
nfan |
|- F/ y ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) |
13 |
|
nfcsb1v |
|- F/_ y [_ E / y ]_ C |
14 |
13
|
a1i |
|- ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> F/_ y [_ E / y ]_ C ) |
15 |
10
|
a1i |
|- ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> F/ y [. E / y ]. ph ) |
16 |
1
|
a1i |
|- ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> D = ( iota_ x e. A A. y e. B ( ph -> x = C ) ) ) |
17 |
|
sbceq1a |
|- ( y = E -> ( ph <-> [. E / y ]. ph ) ) |
18 |
17
|
adantl |
|- ( ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) /\ y = E ) -> ( ph <-> [. E / y ]. ph ) ) |
19 |
|
csbeq1a |
|- ( y = E -> C = [_ E / y ]_ C ) |
20 |
19
|
adantl |
|- ( ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) /\ y = E ) -> C = [_ E / y ]_ C ) |
21 |
|
simpl |
|- ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> D e. A ) |
22 |
|
simprl |
|- ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> E e. B ) |
23 |
|
simprr |
|- ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> [. E / y ]. ph ) |
24 |
12 14 15 16 18 20 21 22 23
|
riotasv2d |
|- ( ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) /\ A e. V ) -> D = [_ E / y ]_ C ) |
25 |
2 3 24
|
syl2anc |
|- ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> D = [_ E / y ]_ C ) |