Theorem rel0 5748

Description: The empty set is a relation. (Contributed by NM, 26-Apr-1998.)

Assertion

Ref	Expression
rel0	⊢ Rel ∅

Proof of Theorem rel0

Step	Hyp	Ref	Expression
1		0ss 4352	. 2 ⊢ ∅ ⊆ (V × V)
2		df-rel 5631	. 2 ⊢ (Rel ∅ ↔ ∅ ⊆ (V × V))
3	1, 2	mpbir 231	1 ⊢ Rel ∅

Syntax hints:  Vcvv 3440   ⊆ wss 3901  ∅c0 4285   × cxp 5622  Rel wrel 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3904  df-ss 3918  df-nul 4286  df-rel 5631

This theorem is referenced by:  relsnb  5751  reldm0  5877  cnveq0  6155  co02  6219  co01  6220  tpos0  8198  0we1  8433  0er  8673  canthwe  10562  relexpreld  14963  disjALTV0  39013  dibvalrel  41423  dicvalrelN  41445  dihvalrel  41539  reldmprcof1  49626  reldmprcof2  49627  reldmlan2  49862  reldmran2  49863  rellan  49868  relran  49869