Metamath Proof Explorer

Theorem elimasngOLD

Description: Obsolete version of elimasng as of 16-Oct-2024. (Contributed by Raph Levien, 21-Oct-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion elimasngOLD 
|- ( ( 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 ) )