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 e. V /\ B e. W ) -> Rel { <. A , B >. } )

Proof

Step	Hyp	Ref	Expression
1		opelvvg	|- ( ( A e. V /\ B e. W ) -> <. A , B >. e. ( _V X. _V ) )
2		opex	|- <. A , B >. e. _V
3		relsng	|- ( <. A , B >. e. _V -> ( Rel { <. A , B >. } <-> <. A , B >. e. ( _V X. _V ) ) )
4	2 3	mp1i	|- ( ( A e. V /\ B e. W ) -> ( Rel { <. A , B >. } <-> <. A , B >. e. ( _V X. _V ) ) )
5	1 4	mpbird	|- ( ( A e. V /\ B e. W ) -> Rel { <. A , B >. } )