Metamath Proof Explorer

Theorem elspansn

Description: Membership in the span of a singleton. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion elspansn 
|- ( A e. ~H -> ( B e. ( span ` { A } ) <-> E. x e. CC B = ( x .h A ) ) )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( A = if ( A e. ~H , A , 0h ) -> { A } = { if ( A e. ~H , A , 0h ) } )
2 1 fveq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( span ` { A } ) = ( span ` { if ( A e. ~H , A , 0h ) } ) )
3 2 eleq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( B e. ( span ` { A } ) <-> B e. ( span ` { if ( A e. ~H , A , 0h ) } ) ) )
4 oveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( x .h A ) = ( x .h if ( A e. ~H , A , 0h ) ) )
5 4 eqeq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( B = ( x .h A ) <-> B = ( x .h if ( A e. ~H , A , 0h ) ) ) )
6 5 rexbidv 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( E. x e. CC B = ( x .h A ) <-> E. x e. CC B = ( x .h if ( A e. ~H , A , 0h ) ) ) )
7 3 6 bibi12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( B e. ( span ` { A } ) <-> E. x e. CC B = ( x .h A ) ) <-> ( B e. ( span ` { if ( A e. ~H , A , 0h ) } ) <-> E. x e. CC B = ( x .h if ( A e. ~H , A , 0h ) ) ) ) )
8 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
9 8 elspansni 
 |-  ( B e. ( span ` { if ( A e. ~H , A , 0h ) } ) <-> E. x e. CC B = ( x .h if ( A e. ~H , A , 0h ) ) )
10 7 9 dedth 
 |-  ( A e. ~H -> ( B e. ( span ` { A } ) <-> E. x e. CC B = ( x .h A ) ) )