Theorem rel0 5743

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

Syntax hints:  Vcvv 3437   ⊆ wss 3898  ∅c0 4282   × cxp 5617  Rel wrel 5624

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-dif 3901  df-ss 3915  df-nul 4283  df-rel 5626

This theorem is referenced by:  relsnb  5746  reldm0  5872  cnveq0  6149  co02  6213  co01  6214  tpos0  8192  0we1  8427  0er  8666  canthwe  10549  relexpreld  14949  disjALTV0  38872  dibvalrel  41282  dicvalrelN  41304  dihvalrel  41398  reldmprcof1  49506  reldmprcof2  49507  reldmlan2  49742  reldmran2  49743  rellan  49748  relran  49749