Metamath Proof Explorer


Theorem elspansni

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

Ref Expression
Hypothesis spansn.1 A
Assertion elspansni BspanAxB=xA

Proof

Step Hyp Ref Expression
1 spansn.1 A
2 1 spansni spanA=A
3 2 eleq2i BspanABA
4 1 h1de2ci BAxB=xA
5 3 4 bitri BspanAxB=xA