Theorem rel0 5738

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 4347	. 2 ⊢ ∅ ⊆ (V × V)
2		df-rel 5621	. 2 ⊢ (Rel ∅ ↔ ∅ ⊆ (V × V))
3	1, 2	mpbir 231	1 ⊢ Rel ∅

Syntax hints:  Vcvv 3436   ⊆ wss 3897  ∅c0 4280   × cxp 5612  Rel wrel 5619

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-dif 3900  df-ss 3914  df-nul 4281  df-rel 5621

This theorem is referenced by:  relsnb  5741  reldm0  5867  cnveq0  6144  co02  6208  co01  6209  tpos0  8186  0we1  8421  0er  8660  canthwe  10542  relexpreld  14947  disjALTV0  38800  dibvalrel  41210  dicvalrelN  41232  dihvalrel  41326  reldmprcof1  49421  reldmprcof2  49422  reldmlan2  49657  reldmran2  49658  rellan  49663  relran  49664