This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ X ∧ B ∈ Y → A B ⟨“ A B ”⟩ ∈ USHGraph

Proof

Step Hyp Ref Expression
1 prex ⊢ A B ∈ V
2 prid1g ⊢ A ∈ X → A ∈ A B
3 prid2g ⊢ B ∈ Y → B ∈ A B
4 uspgr1ewop ⊢ A B ∈ V ∧ A ∈ A B ∧ B ∈ A B → A B ⟨“ A B ”⟩ ∈ USHGraph
5 1 2 3 4 mp3an3an ⊢ A ∈ X ∧ B ∈ Y → A B ⟨“ A B ”⟩ ∈ USHGraph