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 elimasng ⊢ B ∈ V ∧ C ∈ V → C ∈ A B ↔ B C ∈ A
13 df-br ⊢ B A C ↔ B C ∈ A
14 12 13 syl6bbr ⊢ 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