Metamath Proof Explorer

Theorem epnsymrel

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

Ref Expression
Assertion epnsymrel 
|- -. SymRel _E

Proof

Step Hyp Ref Expression
1 epnsym 
 |-  `' _E =/= _E
2 1 neii 
 |-  -. `' _E = _E
3 2 intnanr 
 |-  -. ( `' _E = _E /\ Rel _E )
4 dfsymrel4 
 |-  ( SymRel _E <-> ( `' _E = _E /\ Rel _E ) )
5 3 4 mtbir 
 |-  -. SymRel _E