Theorem epnsymrel

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

	Ref	Expression
Assertion	epnsymrel	$$⊢\neg SymRel\mathrm{E}$$

Proof

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