This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem epnsymrel

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

		Ref	Expression
	Assertion	epnsymrel	$⊢ \neg SymRel E$

Step	Hyp	Ref	Expression
1		epnsym	$⊢ E^{-1} \neq E$
2	1	neii	$⊢ \neg E^{-1} = E$
3	2	intnanr	$⊢ \neg (E^{-1} = E \land Rel E)$
4		dfsymrel4	$⊢ SymRel E \leftrightarrow (E^{-1} = E \land Rel E)$
5	3 4	mtbir	$⊢ \neg SymRel E$