Metamath Proof Explorer


Theorem epnsym

Description: The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022)

Ref Expression
Assertion epnsym E -1 E

Proof

Step Hyp Ref Expression
1 cnvepnep E -1 E =
2 disjeq0 E -1 E = E -1 = E E -1 = E =
3 epn0 E
4 eqneqall E = E E -1 E
5 3 4 mpi E = E -1 E
6 5 adantl E -1 = E = E -1 E
7 6 a1i E -1 = E E -1 = E = E -1 E
8 neqne ¬ E -1 = E E -1 E
9 8 a1d ¬ E -1 = E ¬ E -1 = E = E -1 E
10 7 9 bija E -1 = E E -1 = E = E -1 E
11 1 2 10 mp2b E -1 E