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 ∩ E ) = ∅
2		disjeq0	⊢ ( ( ◡ E ∩ 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