Step |
Hyp |
Ref |
Expression |
1 |
|
scotteqd.1 |
|- ( ph -> A = B ) |
2 |
1
|
adantr |
|- ( ( ph /\ x e. A ) -> A = B ) |
3 |
2
|
raleqdv |
|- ( ( ph /\ x e. A ) -> ( A. y e. A ( rank ` x ) C_ ( rank ` y ) <-> A. y e. B ( rank ` x ) C_ ( rank ` y ) ) ) |
4 |
1 3
|
rabeqbidva |
|- ( ph -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = { x e. B | A. y e. B ( rank ` x ) C_ ( rank ` y ) } ) |
5 |
|
df-scott |
|- Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } |
6 |
|
df-scott |
|- Scott B = { x e. B | A. y e. B ( rank ` x ) C_ ( rank ` y ) } |
7 |
4 5 6
|
3eqtr4g |
|- ( ph -> Scott A = Scott B ) |