Metamath Proof Explorer

Theorem spansneleqi

Description: Membership relation implied by equality of spans. (Contributed by NM, 6-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	spansneleqi	\|- ( A e. ~H -> ( ( span ` { A } ) = ( span ` { B } ) -> A e. ( span ` { B } ) ) )

Step	Hyp	Ref	Expression
1		spansnid	\|- ( A e. ~H -> A e. ( span ` { A } ) )
2		eleq2	\|- ( ( span ` { A } ) = ( span ` { B } ) -> ( A e. ( span ` { A } ) <-> A e. ( span ` { B } ) ) )
3	1 2	syl5ibcom	\|- ( A e. ~H -> ( ( span ` { A } ) = ( span ` { B } ) -> A e. ( span ` { B } ) ) )

Step

Hyp

Ref

Expression

 |-  ( A e. ~H -> A e. ( span ` { A } ) )

 |-  ( ( span ` { A } ) = ( span ` { B } ) -> ( A e. ( span ` { A } ) <-> A e. ( span ` { B } ) ) )

1 2

 |-  ( A e. ~H -> ( ( span ` { A } ) = ( span ` { B } ) -> A e. ( span ` { B } ) ) )