Theorem uspgr2v1e2w

Description: A simple pseudograph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021)

	Ref	Expression
Assertion	uspgr2v1e2w	$$⊢\left(A\in X\wedge B\in Y\right)\to ⟨\left\{A,B\right\},⟨“\left\{A,B\right\}”⟩⟩\in \mathrm{USHGraph}$$

Proof

Step	Hyp	Ref	Expression
1		prex	$$⊢\left\{A,B\right\}\in \mathrm{V}$$
2		prid1g	$$⊢A\in X\to A\in \left\{A,B\right\}$$
3		prid2g	$$⊢B\in Y\to B\in \left\{A,B\right\}$$
4		uspgr1ewop	$$⊢\left(\left\{A,B\right\}\in \mathrm{V}\wedge A\in \left\{A,B\right\}\wedge B\in \left\{A,B\right\}\right)\to ⟨\left\{A,B\right\},⟨“\left\{A,B\right\}”⟩⟩\in \mathrm{USHGraph}$$
5	1 2 3 4	mp3an3an	$$⊢\left(A\in X\wedge B\in Y\right)\to ⟨\left\{A,B\right\},⟨“\left\{A,B\right\}”⟩⟩\in \mathrm{USHGraph}$$