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	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ⟨ { 𝐴 , 𝐵 } , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ ∈ USPGraph )

Proof

Step	Hyp	Ref	Expression
1		prex	⊢ { 𝐴 , 𝐵 } ∈ V
2		prid1g	⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐴 , 𝐵 } )
3		prid2g	⊢ ( 𝐵 ∈ 𝑌 → 𝐵 ∈ { 𝐴 , 𝐵 } )
4		uspgr1ewop	⊢ ( ( { 𝐴 , 𝐵 } ∈ V ∧ 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) → ⟨ { 𝐴 , 𝐵 } , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ ∈ USPGraph )
5	1 2 3 4	mp3an3an	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ⟨ { 𝐴 , 𝐵 } , ⟨“ { 𝐴 , 𝐵 } ”⟩ ⟩ ∈ USPGraph )