Step |
Hyp |
Ref |
Expression |
1 |
|
t1sep.1 |
|- X = U. J |
2 |
|
simpr3 |
|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> A =/= B ) |
3 |
1
|
t1sep2 |
|- ( ( J e. Fre /\ A e. X /\ B e. X ) -> ( A. o e. J ( A e. o -> B e. o ) -> A = B ) ) |
4 |
3
|
3adant3r3 |
|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> ( A. o e. J ( A e. o -> B e. o ) -> A = B ) ) |
5 |
4
|
necon3ad |
|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> ( A =/= B -> -. A. o e. J ( A e. o -> B e. o ) ) ) |
6 |
2 5
|
mpd |
|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> -. A. o e. J ( A e. o -> B e. o ) ) |
7 |
|
rexanali |
|- ( E. o e. J ( A e. o /\ -. B e. o ) <-> -. A. o e. J ( A e. o -> B e. o ) ) |
8 |
6 7
|
sylibr |
|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> E. o e. J ( A e. o /\ -. B e. o ) ) |