Step |
Hyp |
Ref |
Expression |
1 |
|
rabxfrd.1 |
|- F/_ y B |
2 |
|
rabxfrd.2 |
|- F/_ y C |
3 |
|
rabxfrd.3 |
|- ( ( ph /\ y e. D ) -> A e. D ) |
4 |
|
rabxfrd.4 |
|- ( x = A -> ( ps <-> ch ) ) |
5 |
|
rabxfrd.5 |
|- ( y = B -> A = C ) |
6 |
3
|
ex |
|- ( ph -> ( y e. D -> A e. D ) ) |
7 |
|
ibibr |
|- ( ( y e. D -> A e. D ) <-> ( y e. D -> ( A e. D <-> y e. D ) ) ) |
8 |
6 7
|
sylib |
|- ( ph -> ( y e. D -> ( A e. D <-> y e. D ) ) ) |
9 |
8
|
imp |
|- ( ( ph /\ y e. D ) -> ( A e. D <-> y e. D ) ) |
10 |
9
|
anbi1d |
|- ( ( ph /\ y e. D ) -> ( ( A e. D /\ ch ) <-> ( y e. D /\ ch ) ) ) |
11 |
4
|
elrab |
|- ( A e. { x e. D | ps } <-> ( A e. D /\ ch ) ) |
12 |
|
rabid |
|- ( y e. { y e. D | ch } <-> ( y e. D /\ ch ) ) |
13 |
10 11 12
|
3bitr4g |
|- ( ( ph /\ y e. D ) -> ( A e. { x e. D | ps } <-> y e. { y e. D | ch } ) ) |
14 |
13
|
rabbidva |
|- ( ph -> { y e. D | A e. { x e. D | ps } } = { y e. D | y e. { y e. D | ch } } ) |
15 |
14
|
eleq2d |
|- ( ph -> ( B e. { y e. D | A e. { x e. D | ps } } <-> B e. { y e. D | y e. { y e. D | ch } } ) ) |
16 |
|
nfcv |
|- F/_ y D |
17 |
2
|
nfel1 |
|- F/ y C e. { x e. D | ps } |
18 |
5
|
eleq1d |
|- ( y = B -> ( A e. { x e. D | ps } <-> C e. { x e. D | ps } ) ) |
19 |
1 16 17 18
|
elrabf |
|- ( B e. { y e. D | A e. { x e. D | ps } } <-> ( B e. D /\ C e. { x e. D | ps } ) ) |
20 |
|
nfrab1 |
|- F/_ y { y e. D | ch } |
21 |
1 20
|
nfel |
|- F/ y B e. { y e. D | ch } |
22 |
|
eleq1 |
|- ( y = B -> ( y e. { y e. D | ch } <-> B e. { y e. D | ch } ) ) |
23 |
1 16 21 22
|
elrabf |
|- ( B e. { y e. D | y e. { y e. D | ch } } <-> ( B e. D /\ B e. { y e. D | ch } ) ) |
24 |
15 19 23
|
3bitr3g |
|- ( ph -> ( ( B e. D /\ C e. { x e. D | ps } ) <-> ( B e. D /\ B e. { y e. D | ch } ) ) ) |
25 |
|
pm5.32 |
|- ( ( B e. D -> ( C e. { x e. D | ps } <-> B e. { y e. D | ch } ) ) <-> ( ( B e. D /\ C e. { x e. D | ps } ) <-> ( B e. D /\ B e. { y e. D | ch } ) ) ) |
26 |
24 25
|
sylibr |
|- ( ph -> ( B e. D -> ( C e. { x e. D | ps } <-> B e. { y e. D | ch } ) ) ) |
27 |
26
|
imp |
|- ( ( ph /\ B e. D ) -> ( C e. { x e. D | ps } <-> B e. { y e. D | ch } ) ) |