Step |
Hyp |
Ref |
Expression |
1 |
|
dfepfr |
|- ( _E Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) ) |
2 |
|
vex |
|- x e. _V |
3 |
|
zfreg |
|- ( ( x e. _V /\ x =/= (/) ) -> E. y e. x ( y i^i x ) = (/) ) |
4 |
2 3
|
mpan |
|- ( x =/= (/) -> E. y e. x ( y i^i x ) = (/) ) |
5 |
|
incom |
|- ( y i^i x ) = ( x i^i y ) |
6 |
5
|
eqeq1i |
|- ( ( y i^i x ) = (/) <-> ( x i^i y ) = (/) ) |
7 |
6
|
rexbii |
|- ( E. y e. x ( y i^i x ) = (/) <-> E. y e. x ( x i^i y ) = (/) ) |
8 |
4 7
|
sylib |
|- ( x =/= (/) -> E. y e. x ( x i^i y ) = (/) ) |
9 |
8
|
adantl |
|- ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) |
10 |
1 9
|
mpgbir |
|- _E Fr A |