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

Metamath Proof Explorer

Theorem relsnopg

Description: A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998) (Revised by BJ, 12-Feb-2022)

Ref Expression
Assertion relsnopg ⊢ A ∈ V ∧ B ∈ W → Rel ⁡ A B

Proof

Step Hyp Ref Expression
1 opelvvg ⊢ A ∈ V ∧ B ∈ W → A B ∈ V × V
2 opex ⊢ A B ∈ V
3 relsng ⊢ A B ∈ V → Rel ⁡ A B ↔ A B ∈ V × V
4 2 3 mp1i ⊢ A ∈ V ∧ B ∈ W → Rel ⁡ A B ↔ A B ∈ V × V
5 1 4 mpbird ⊢ A ∈ V ∧ B ∈ W → Rel ⁡ A B