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