Metamath Proof Explorer

Theorem elimasni

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

Ref Expression
Assertion elimasni 
|- ( C e. ( A " { B } ) -> B A C )

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. C e. (/)
2 snprc 
 |-  ( -. B e. _V <-> { B } = (/) )
3 2 biimpi 
 |-  ( -. B e. _V -> { B } = (/) )
4 3 imaeq2d 
 |-  ( -. B e. _V -> ( A " { B } ) = ( A " (/) ) )
5 ima0 
 |-  ( A " (/) ) = (/)
6 4 5 eqtrdi 
 |-  ( -. B e. _V -> ( A " { B } ) = (/) )
7 6 eleq2d 
 |-  ( -. B e. _V -> ( C e. ( A " { B } ) <-> C e. (/) ) )
8 1 7 mtbiri 
 |-  ( -. B e. _V -> -. C e. ( A " { B } ) )
9 8 con4i 
 |-  ( C e. ( A " { B } ) -> B e. _V )
10 elex 
 |-  ( C e. ( A " { B } ) -> C e. _V )
11 9 10 jca 
 |-  ( C e. ( A " { B } ) -> ( B e. _V /\ C e. _V ) )
12 elimasng1 
 |-  ( ( B e. _V /\ C e. _V ) -> ( C e. ( A " { B } ) <-> B A C ) )
13 12 biimpd 
 |-  ( ( B e. _V /\ C e. _V ) -> ( C e. ( A " { B } ) -> B A C ) )
14 11 13 mpcom 
 |-  ( C e. ( A " { B } ) -> B A C )