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	|- ( ( A e. X /\ B e. Y ) -> <. { A , B } , <" { A , B } "> >. e. USPGraph )

Proof

Step	Hyp	Ref	Expression
1		prex	|- { A , B } e. _V
2		prid1g	|- ( A e. X -> A e. { A , B } )
3		prid2g	|- ( B e. Y -> B e. { A , B } )
4		uspgr1ewop	|- ( ( { A , B } e. _V /\ A e. { A , B } /\ B e. { A , B } ) -> <. { A , B } , <" { A , B } "> >. e. USPGraph )
5	1 2 3 4	mp3an3an	|- ( ( A e. X /\ B e. Y ) -> <. { A , B } , <" { A , B } "> >. e. USPGraph )