Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Regularity
Introduce the Axiom of Regularity
epnsym
Next ⟩
elnotel
Metamath Proof Explorer
Ascii
Unicode
Theorem
epnsym
Description:
The membership (epsilon) relation is not symmetric.
(Contributed by
AV
, 18-Jun-2022)
Ref
Expression
Assertion
epnsym
⊢
E
-1
≠
E
Proof
Step
Hyp
Ref
Expression
1
cnvepnep
⊢
E
-1
∩
E
=
∅
2
disjeq0
⊢
E
-1
∩
E
=
∅
→
E
-1
=
E
↔
E
-1
=
∅
∧
E
=
∅
3
epn0
⊢
E
≠
∅
4
eqneqall
⊢
E
=
∅
→
E
≠
∅
→
E
-1
≠
E
5
3
4
mpi
⊢
E
=
∅
→
E
-1
≠
E
6
5
adantl
⊢
E
-1
=
∅
∧
E
=
∅
→
E
-1
≠
E
7
6
a1i
⊢
E
-1
=
E
→
E
-1
=
∅
∧
E
=
∅
→
E
-1
≠
E
8
neqne
⊢
¬
E
-1
=
E
→
E
-1
≠
E
9
8
a1d
⊢
¬
E
-1
=
E
→
¬
E
-1
=
∅
∧
E
=
∅
→
E
-1
≠
E
10
7
9
bija
⊢
E
-1
=
E
↔
E
-1
=
∅
∧
E
=
∅
→
E
-1
≠
E
11
1
2
10
mp2b
⊢
E
-1
≠
E