Step |
Hyp |
Ref |
Expression |
1 |
|
dfcleq |
|- ( A = B <-> A. x ( x e. A <-> x e. B ) ) |
2 |
1
|
biimpi |
|- ( A = B -> A. x ( x e. A <-> x e. B ) ) |
3 |
|
anbi1 |
|- ( ( x e. A <-> x e. B ) -> ( ( x e. A /\ ph ) <-> ( x e. B /\ ph ) ) ) |
4 |
3
|
imbi1d |
|- ( ( x e. A <-> x e. B ) -> ( ( ( x e. A /\ ph ) -> x = z ) <-> ( ( x e. B /\ ph ) -> x = z ) ) ) |
5 |
4
|
alimi |
|- ( A. x ( x e. A <-> x e. B ) -> A. x ( ( ( x e. A /\ ph ) -> x = z ) <-> ( ( x e. B /\ ph ) -> x = z ) ) ) |
6 |
|
albi |
|- ( A. x ( ( ( x e. A /\ ph ) -> x = z ) <-> ( ( x e. B /\ ph ) -> x = z ) ) -> ( A. x ( ( x e. A /\ ph ) -> x = z ) <-> A. x ( ( x e. B /\ ph ) -> x = z ) ) ) |
7 |
2 5 6
|
3syl |
|- ( A = B -> ( A. x ( ( x e. A /\ ph ) -> x = z ) <-> A. x ( ( x e. B /\ ph ) -> x = z ) ) ) |
8 |
7
|
exbidv |
|- ( A = B -> ( E. z A. x ( ( x e. A /\ ph ) -> x = z ) <-> E. z A. x ( ( x e. B /\ ph ) -> x = z ) ) ) |
9 |
|
df-mo |
|- ( E* x ( x e. A /\ ph ) <-> E. z A. x ( ( x e. A /\ ph ) -> x = z ) ) |
10 |
|
df-mo |
|- ( E* x ( x e. B /\ ph ) <-> E. z A. x ( ( x e. B /\ ph ) -> x = z ) ) |
11 |
8 9 10
|
3bitr4g |
|- ( A = B -> ( E* x ( x e. A /\ ph ) <-> E* x ( x e. B /\ ph ) ) ) |
12 |
|
df-rmo |
|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) ) |
13 |
|
df-rmo |
|- ( E* x e. B ph <-> E* x ( x e. B /\ ph ) ) |
14 |
11 12 13
|
3bitr4g |
|- ( A = B -> ( E* x e. A ph <-> E* x e. B ph ) ) |