This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elimasni

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

Ref Expression
Assertion elimasni ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) → 𝐵 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 noel ⊢ ¬ 𝐶 ∈ ∅
2 snprc ⊢ ( ¬ 𝐵 ∈ V ↔ { 𝐵 } = ∅ )
3 2 biimpi ⊢ ( ¬ 𝐵 ∈ V → { 𝐵 } = ∅ )
4 3 imaeq2d ⊢ ( ¬ 𝐵 ∈ V → ( 𝐴 “ { 𝐵 } ) = ( 𝐴 “ ∅ ) )
5 ima0 ⊢ ( 𝐴 “ ∅ ) = ∅
6 4 5 eqtrdi ⊢ ( ¬ 𝐵 ∈ V → ( 𝐴 “ { 𝐵 } ) = ∅ )
7 6 eleq2d ⊢ ( ¬ 𝐵 ∈ V → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐶 ∈ ∅ ) )
8 1 7 mtbiri ⊢ ( ¬ 𝐵 ∈ V → ¬ 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) )
9 8 con4i ⊢ ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) → 𝐵 ∈ V )
10 elex ⊢ ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) → 𝐶 ∈ V )
11 9 10 jca ⊢ ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) )
12 elimasng1 ⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐵 𝐴 𝐶 ) )
13 12 biimpd ⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) → 𝐵 𝐴 𝐶 ) )
14 11 13 mpcom ⊢ ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) → 𝐵 𝐴 𝐶 )