Theorem rel0 5746

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

Syntax hints:  Vcvv 3438   ⊆ wss 3899  ∅c0 4283   × cxp 5620  Rel wrel 5627

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-dif 3902  df-ss 3916  df-nul 4284  df-rel 5629

This theorem is referenced by:  relsnb  5749  reldm0  5875  cnveq0  6153  co02  6217  co01  6218  tpos0  8196  0we1  8431  0er  8671  canthwe  10560  relexpreld  14961  disjALTV0  38952  dibvalrel  41362  dicvalrelN  41384  dihvalrel  41478  reldmprcof1  49568  reldmprcof2  49569  reldmlan2  49804  reldmran2  49805  rellan  49810  relran  49811