Metamath Proof Explorer

Theorem elimasni

Description: Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010)

Ref Expression
Assertion elimasni ⊢C∈AB→BAC

Proof

Step Hyp Ref Expression
1 noel ⊢¬C∈∅
2 snprc ⊢¬B∈V↔B=∅
3 2 biimpi ⊢¬B∈V→B=∅
4 3 imaeq2d ⊢¬B∈V→AB=A∅
5 ima0 ⊢A∅=∅
6 4 5 eqtrdi ⊢¬B∈V→AB=∅
7 6 eleq2d ⊢¬B∈V→C∈AB↔C∈∅
8 1 7 mtbiri ⊢¬B∈V→¬C∈AB
9 8 con4i ⊢C∈AB→B∈V
10 elex ⊢C∈AB→C∈V
11 9 10 jca ⊢C∈AB→B∈V∧C∈V
12 elimasng1 ⊢B∈V∧C∈V→C∈AB↔BAC
13 12 biimpd ⊢B∈V∧C∈V→C∈AB→BAC
14 11 13 mpcom ⊢C∈AB→BAC