Metamath Proof Explorer

Theorem elimasng

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006)

Ref Expression
Assertion elimasng 
|- ( ( B e. V /\ C e. W ) -> ( C e. ( A " { B } ) <-> <. B , C >. e. A ) )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( y = B -> { y } = { B } )
2 1 imaeq2d 
 |-  ( y = B -> ( A " { y } ) = ( A " { B } ) )
3 2 eleq2d 
 |-  ( y = B -> ( z e. ( A " { y } ) <-> z e. ( A " { B } ) ) )
4 opeq1 
 |-  ( y = B -> <. y , z >. = <. B , z >. )
5 4 eleq1d 
 |-  ( y = B -> ( <. y , z >. e. A <-> <. B , z >. e. A ) )
6 3 5 bibi12d 
 |-  ( y = B -> ( ( z e. ( A " { y } ) <-> <. y , z >. e. A ) <-> ( z e. ( A " { B } ) <-> <. B , z >. e. A ) ) )
7 eleq1 
 |-  ( z = C -> ( z e. ( A " { B } ) <-> C e. ( A " { B } ) ) )
8 opeq2 
 |-  ( z = C -> <. B , z >. = <. B , C >. )
9 8 eleq1d 
 |-  ( z = C -> ( <. B , z >. e. A <-> <. B , C >. e. A ) )
10 7 9 bibi12d 
 |-  ( z = C -> ( ( z e. ( A " { B } ) <-> <. B , z >. e. A ) <-> ( C e. ( A " { B } ) <-> <. B , C >. e. A ) ) )
11 vex 
 |-  y e. _V
12 vex 
 |-  z e. _V
13 11 12 elimasn 
 |-  ( z e. ( A " { y } ) <-> <. y , z >. e. A )
14 6 10 13 vtocl2g 
 |-  ( ( B e. V /\ C e. W ) -> ( C e. ( A " { B } ) <-> <. B , C >. e. A ) )