Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
|- ( A e. P. -> A e. _V ) |
2 |
|
simpl1 |
|- ( ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x A e. _V ) |
3 |
|
psseq2 |
|- ( z = w -> ( (/) C. z <-> (/) C. w ) ) |
4 |
|
psseq1 |
|- ( z = w -> ( z C. Q. <-> w C. Q. ) ) |
5 |
3 4
|
anbi12d |
|- ( z = w -> ( ( (/) C. z /\ z C. Q. ) <-> ( (/) C. w /\ w C. Q. ) ) ) |
6 |
|
elequ2 |
|- ( z = w -> ( y e. z <-> y e. w ) ) |
7 |
6
|
imbi2d |
|- ( z = w -> ( ( y y e. z ) <-> ( y y e. w ) ) ) |
8 |
7
|
albidv |
|- ( z = w -> ( A. y ( y y e. z ) <-> A. y ( y y e. w ) ) ) |
9 |
|
rexeq |
|- ( z = w -> ( E. y e. z x E. y e. w x |
10 |
8 9
|
anbi12d |
|- ( z = w -> ( ( A. y ( y y e. z ) /\ E. y e. z x ( A. y ( y y e. w ) /\ E. y e. w x |
11 |
10
|
raleqbi1dv |
|- ( z = w -> ( A. x e. z ( A. y ( y y e. z ) /\ E. y e. z x A. x e. w ( A. y ( y y e. w ) /\ E. y e. w x |
12 |
5 11
|
anbi12d |
|- ( z = w -> ( ( ( (/) C. z /\ z C. Q. ) /\ A. x e. z ( A. y ( y y e. z ) /\ E. y e. z x ( ( (/) C. w /\ w C. Q. ) /\ A. x e. w ( A. y ( y y e. w ) /\ E. y e. w x |
13 |
|
psseq2 |
|- ( w = A -> ( (/) C. w <-> (/) C. A ) ) |
14 |
|
psseq1 |
|- ( w = A -> ( w C. Q. <-> A C. Q. ) ) |
15 |
13 14
|
anbi12d |
|- ( w = A -> ( ( (/) C. w /\ w C. Q. ) <-> ( (/) C. A /\ A C. Q. ) ) ) |
16 |
|
eleq2 |
|- ( w = A -> ( y e. w <-> y e. A ) ) |
17 |
16
|
imbi2d |
|- ( w = A -> ( ( y y e. w ) <-> ( y y e. A ) ) ) |
18 |
17
|
albidv |
|- ( w = A -> ( A. y ( y y e. w ) <-> A. y ( y y e. A ) ) ) |
19 |
|
rexeq |
|- ( w = A -> ( E. y e. w x E. y e. A x |
20 |
18 19
|
anbi12d |
|- ( w = A -> ( ( A. y ( y y e. w ) /\ E. y e. w x ( A. y ( y y e. A ) /\ E. y e. A x |
21 |
20
|
raleqbi1dv |
|- ( w = A -> ( A. x e. w ( A. y ( y y e. w ) /\ E. y e. w x A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x |
22 |
15 21
|
anbi12d |
|- ( w = A -> ( ( ( (/) C. w /\ w C. Q. ) /\ A. x e. w ( A. y ( y y e. w ) /\ E. y e. w x ( ( (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x |
23 |
|
df-np |
|- P. = { z | ( ( (/) C. z /\ z C. Q. ) /\ A. x e. z ( A. y ( y y e. z ) /\ E. y e. z x |
24 |
12 22 23
|
elab2gw |
|- ( A e. _V -> ( A e. P. <-> ( ( (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x |
25 |
|
id |
|- ( ( A e. _V /\ (/) C. A /\ A C. Q. ) -> ( A e. _V /\ (/) C. A /\ A C. Q. ) ) |
26 |
25
|
3expib |
|- ( A e. _V -> ( ( (/) C. A /\ A C. Q. ) -> ( A e. _V /\ (/) C. A /\ A C. Q. ) ) ) |
27 |
|
3simpc |
|- ( ( A e. _V /\ (/) C. A /\ A C. Q. ) -> ( (/) C. A /\ A C. Q. ) ) |
28 |
26 27
|
impbid1 |
|- ( A e. _V -> ( ( (/) C. A /\ A C. Q. ) <-> ( A e. _V /\ (/) C. A /\ A C. Q. ) ) ) |
29 |
28
|
anbi1d |
|- ( A e. _V -> ( ( ( (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x |
30 |
24 29
|
bitrd |
|- ( A e. _V -> ( A e. P. <-> ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x |
31 |
1 2 30
|
pm5.21nii |
|- ( A e. P. <-> ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x |