Metamath Proof Explorer

Theorem epnsym

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

Ref Expression
Assertion epnsym 
|- `' _E =/= _E

Proof

Step Hyp Ref Expression
1 cnvepnep 
 |-  ( `' _E i^i _E ) = (/)
2 disjeq0 
 |-  ( ( `' _E i^i _E ) = (/) -> ( `' _E = _E <-> ( `' _E = (/) /\ _E = (/) ) ) )
3 epn0 
 |-  _E =/= (/)
4 eqneqall 
 |-  ( _E = (/) -> ( _E =/= (/) -> `' _E =/= _E ) )
5 3 4 mpi 
 |-  ( _E = (/) -> `' _E =/= _E )
6 5 adantl 
 |-  ( ( `' _E = (/) /\ _E = (/) ) -> `' _E =/= _E )
7 6 a1i 
 |-  ( `' _E = _E -> ( ( `' _E = (/) /\ _E = (/) ) -> `' _E =/= _E ) )
8 neqne 
 |-  ( -. `' _E = _E -> `' _E =/= _E )
9 8 a1d 
 |-  ( -. `' _E = _E -> ( -. ( `' _E = (/) /\ _E = (/) ) -> `' _E =/= _E ) )
10 7 9 bija 
 |-  ( ( `' _E = _E <-> ( `' _E = (/) /\ _E = (/) ) ) -> `' _E =/= _E )
11 1 2 10 mp2b 
 |-  `' _E =/= _E