Step |
Hyp |
Ref |
Expression |
1 |
|
sbc3or |
|- ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) |
2 |
|
sbcel2gv |
|- ( A e. V -> ( [. A / y ]. x e. y <-> x e. A ) ) |
3 |
|
sbcel1v |
|- ( [. A / y ]. y e. x <-> A e. x ) |
4 |
3
|
a1i |
|- ( A e. V -> ( [. A / y ]. y e. x <-> A e. x ) ) |
5 |
|
eqsbc3r |
|- ( A e. V -> ( [. A / y ]. x = y <-> x = A ) ) |
6 |
|
3orbi123 |
|- ( ( ( [. A / y ]. x e. y <-> x e. A ) /\ ( [. A / y ]. y e. x <-> A e. x ) /\ ( [. A / y ]. x = y <-> x = A ) ) -> ( ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) ) |
7 |
6
|
3impexpbicomi |
|- ( ( [. A / y ]. x e. y <-> x e. A ) -> ( ( [. A / y ]. y e. x <-> A e. x ) -> ( ( [. A / y ]. x = y <-> x = A ) -> ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ) ) ) |
8 |
2 4 5 7
|
syl3c |
|- ( A e. V -> ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ) |
9 |
1 8
|
bitr4id |
|- ( A e. V -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) ) |