Step |
Hyp |
Ref |
Expression |
1 |
|
nfrab1 |
|- F/_ y { y e. B | ph } |
2 |
|
nfcv |
|- F/_ z { y e. B | ph } |
3 |
|
nfv |
|- F/ z C e. A |
4 |
|
nfcsb1v |
|- F/_ y [_ z / y ]_ C |
5 |
4
|
nfel1 |
|- F/ y [_ z / y ]_ C e. A |
6 |
|
csbeq1a |
|- ( y = z -> C = [_ z / y ]_ C ) |
7 |
6
|
eleq1d |
|- ( y = z -> ( C e. A <-> [_ z / y ]_ C e. A ) ) |
8 |
1 2 3 5 7
|
cbvralfw |
|- ( A. y e. { y e. B | ph } C e. A <-> A. z e. { y e. B | ph } [_ z / y ]_ C e. A ) |
9 |
|
rabid |
|- ( y e. { y e. B | ph } <-> ( y e. B /\ ph ) ) |
10 |
9
|
imbi1i |
|- ( ( y e. { y e. B | ph } -> C e. A ) <-> ( ( y e. B /\ ph ) -> C e. A ) ) |
11 |
|
impexp |
|- ( ( ( y e. B /\ ph ) -> C e. A ) <-> ( y e. B -> ( ph -> C e. A ) ) ) |
12 |
10 11
|
bitri |
|- ( ( y e. { y e. B | ph } -> C e. A ) <-> ( y e. B -> ( ph -> C e. A ) ) ) |
13 |
12
|
ralbii2 |
|- ( A. y e. { y e. B | ph } C e. A <-> A. y e. B ( ph -> C e. A ) ) |
14 |
8 13
|
bitr3i |
|- ( A. z e. { y e. B | ph } [_ z / y ]_ C e. A <-> A. y e. B ( ph -> C e. A ) ) |
15 |
|
rabn0 |
|- ( { y e. B | ph } =/= (/) <-> E. y e. B ph ) |
16 |
|
reusv2lem5 |
|- ( ( A. z e. { y e. B | ph } [_ z / y ]_ C e. A /\ { y e. B | ph } =/= (/) ) -> ( E! x e. A E. z e. { y e. B | ph } x = [_ z / y ]_ C <-> E! x e. A A. z e. { y e. B | ph } x = [_ z / y ]_ C ) ) |
17 |
|
nfv |
|- F/ z x = C |
18 |
4
|
nfeq2 |
|- F/ y x = [_ z / y ]_ C |
19 |
6
|
eqeq2d |
|- ( y = z -> ( x = C <-> x = [_ z / y ]_ C ) ) |
20 |
1 2 17 18 19
|
cbvrexfw |
|- ( E. y e. { y e. B | ph } x = C <-> E. z e. { y e. B | ph } x = [_ z / y ]_ C ) |
21 |
9
|
anbi1i |
|- ( ( y e. { y e. B | ph } /\ x = C ) <-> ( ( y e. B /\ ph ) /\ x = C ) ) |
22 |
|
anass |
|- ( ( ( y e. B /\ ph ) /\ x = C ) <-> ( y e. B /\ ( ph /\ x = C ) ) ) |
23 |
21 22
|
bitri |
|- ( ( y e. { y e. B | ph } /\ x = C ) <-> ( y e. B /\ ( ph /\ x = C ) ) ) |
24 |
23
|
rexbii2 |
|- ( E. y e. { y e. B | ph } x = C <-> E. y e. B ( ph /\ x = C ) ) |
25 |
20 24
|
bitr3i |
|- ( E. z e. { y e. B | ph } x = [_ z / y ]_ C <-> E. y e. B ( ph /\ x = C ) ) |
26 |
25
|
reubii |
|- ( E! x e. A E. z e. { y e. B | ph } x = [_ z / y ]_ C <-> E! x e. A E. y e. B ( ph /\ x = C ) ) |
27 |
1 2 17 18 19
|
cbvralfw |
|- ( A. y e. { y e. B | ph } x = C <-> A. z e. { y e. B | ph } x = [_ z / y ]_ C ) |
28 |
9
|
imbi1i |
|- ( ( y e. { y e. B | ph } -> x = C ) <-> ( ( y e. B /\ ph ) -> x = C ) ) |
29 |
|
impexp |
|- ( ( ( y e. B /\ ph ) -> x = C ) <-> ( y e. B -> ( ph -> x = C ) ) ) |
30 |
28 29
|
bitri |
|- ( ( y e. { y e. B | ph } -> x = C ) <-> ( y e. B -> ( ph -> x = C ) ) ) |
31 |
30
|
ralbii2 |
|- ( A. y e. { y e. B | ph } x = C <-> A. y e. B ( ph -> x = C ) ) |
32 |
27 31
|
bitr3i |
|- ( A. z e. { y e. B | ph } x = [_ z / y ]_ C <-> A. y e. B ( ph -> x = C ) ) |
33 |
32
|
reubii |
|- ( E! x e. A A. z e. { y e. B | ph } x = [_ z / y ]_ C <-> E! x e. A A. y e. B ( ph -> x = C ) ) |
34 |
16 26 33
|
3bitr3g |
|- ( ( A. z e. { y e. B | ph } [_ z / y ]_ C e. A /\ { y e. B | ph } =/= (/) ) -> ( E! x e. A E. y e. B ( ph /\ x = C ) <-> E! x e. A A. y e. B ( ph -> x = C ) ) ) |
35 |
14 15 34
|
syl2anbr |
|- ( ( A. y e. B ( ph -> C e. A ) /\ E. y e. B ph ) -> ( E! x e. A E. y e. B ( ph /\ x = C ) <-> E! x e. A A. y e. B ( ph -> x = C ) ) ) |