Theorem rel0 5742

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

Syntax hints:  Vcvv 3431   ⊆ wss 3883  ∅c0 4261   × cxp 5616  Rel wrel 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-dif 3886  df-ss 3900  df-nul 4262  df-rel 5625

This theorem is referenced by:  relsnb  5745  reldm0  5870  cnveq0  6148  co02  6212  co01  6213  tpos0  8196  0we1  8431  0er  8672  canthwe  10565  relexpreld  14993  disjALTV0  39221  dibvalrel  41655  dicvalrelN  41677  dihvalrel  41771  reldmprcof1  49871  reldmprcof2  49872  reldmlan2  50107  reldmran2  50108  rellan  50113  relran  50114