Step |
Hyp |
Ref |
Expression |
1 |
|
dffr2 |
|- ( _E Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z _E y } = (/) ) ) |
2 |
|
epel |
|- ( z _E y <-> z e. y ) |
3 |
2
|
rabbii |
|- { z e. x | z _E y } = { z e. x | z e. y } |
4 |
|
dfin5 |
|- ( x i^i y ) = { z e. x | z e. y } |
5 |
3 4
|
eqtr4i |
|- { z e. x | z _E y } = ( x i^i y ) |
6 |
5
|
eqeq1i |
|- ( { z e. x | z _E y } = (/) <-> ( x i^i y ) = (/) ) |
7 |
6
|
rexbii |
|- ( E. y e. x { z e. x | z _E y } = (/) <-> E. y e. x ( x i^i y ) = (/) ) |
8 |
7
|
imbi2i |
|- ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z _E y } = (/) ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) ) |
9 |
8
|
albii |
|- ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z _E y } = (/) ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) ) |
10 |
1 9
|
bitri |
|- ( _E Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) ) |