Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Relations
elimasng
Next ⟩
elimasni
Metamath Proof Explorer
Ascii
Unicode
Theorem
elimasng
Description:
Membership in an image of a singleton.
(Contributed by
Raph Levien
, 21-Oct-2006)
Ref
Expression
Assertion
elimasng
⊢
B
∈
V
∧
C
∈
W
→
C
∈
A
B
↔
B
C
∈
A
Proof
Step
Hyp
Ref
Expression
1
sneq
⊢
y
=
B
→
y
=
B
2
1
imaeq2d
⊢
y
=
B
→
A
y
=
A
B
3
2
eleq2d
⊢
y
=
B
→
z
∈
A
y
↔
z
∈
A
B
4
opeq1
⊢
y
=
B
→
y
z
=
B
z
5
4
eleq1d
⊢
y
=
B
→
y
z
∈
A
↔
B
z
∈
A
6
3
5
bibi12d
⊢
y
=
B
→
z
∈
A
y
↔
y
z
∈
A
↔
z
∈
A
B
↔
B
z
∈
A
7
eleq1
⊢
z
=
C
→
z
∈
A
B
↔
C
∈
A
B
8
opeq2
⊢
z
=
C
→
B
z
=
B
C
9
8
eleq1d
⊢
z
=
C
→
B
z
∈
A
↔
B
C
∈
A
10
7
9
bibi12d
⊢
z
=
C
→
z
∈
A
B
↔
B
z
∈
A
↔
C
∈
A
B
↔
B
C
∈
A
11
vex
⊢
y
∈
V
12
vex
⊢
z
∈
V
13
11
12
elimasn
⊢
z
∈
A
y
↔
y
z
∈
A
14
6
10
13
vtocl2g
⊢
B
∈
V
∧
C
∈
W
→
C
∈
A
B
↔
B
C
∈
A