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 syl6eq 
 |-  ( -. 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 elimasng 
 |-  ( ( B e. _V /\ C e. _V ) -> ( C e. ( A " { B } ) <-> <. B , C >. e. A ) )
13 df-br 
 |-  ( B A C <-> <. B , C >. e. A )
14 12 13 syl6bbr 
 |-  ( ( B e. _V /\ C e. _V ) -> ( C e. ( A " { B } ) <-> B A C ) )
15 14 biimpd 
 |-  ( ( B e. _V /\ C e. _V ) -> ( C e. ( A " { B } ) -> B A C ) )
16 11 15 mpcom 
 |-  ( C e. ( A " { B } ) -> B A C )