Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Relations
elimasni
Next ⟩
args
Metamath Proof Explorer
Ascii
Unicode
Theorem
elimasni
Description:
Membership in an image of a singleton.
(Contributed by
NM
, 5-Aug-2010)
Ref
Expression
Assertion
elimasni
⊢
C
∈
A
B
→
B
A
C
Proof
Step
Hyp
Ref
Expression
1
noel
⊢
¬
C
∈
∅
2
snprc
⊢
¬
B
∈
V
↔
B
=
∅
3
2
biimpi
⊢
¬
B
∈
V
→
B
=
∅
4
3
imaeq2d
⊢
¬
B
∈
V
→
A
B
=
A
∅
5
ima0
⊢
A
∅
=
∅
6
4
5
eqtrdi
⊢
¬
B
∈
V
→
A
B
=
∅
7
6
eleq2d
⊢
¬
B
∈
V
→
C
∈
A
B
↔
C
∈
∅
8
1
7
mtbiri
⊢
¬
B
∈
V
→
¬
C
∈
A
B
9
8
con4i
⊢
C
∈
A
B
→
B
∈
V
10
elex
⊢
C
∈
A
B
→
C
∈
V
11
9
10
jca
⊢
C
∈
A
B
→
B
∈
V
∧
C
∈
V
12
elimasng
⊢
B
∈
V
∧
C
∈
V
→
C
∈
A
B
↔
B
C
∈
A
13
df-br
⊢
B
A
C
↔
B
C
∈
A
14
12
13
bitr4di
⊢
B
∈
V
∧
C
∈
V
→
C
∈
A
B
↔
B
A
C
15
14
biimpd
⊢
B
∈
V
∧
C
∈
V
→
C
∈
A
B
→
B
A
C
16
11
15
mpcom
⊢
C
∈
A
B
→
B
A
C