Metamath Proof Explorer

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 elimasng1 ⊢ B ∈ V ∧ C ∈ V → C ∈ A B ↔ B A C
13 12 biimpd ⊢ B ∈ V ∧ C ∈ V → C ∈ A B → B A C
14 11 13 mpcom ⊢ C ∈ A B → B A C