Theorem rel0 5777

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 5658	. 2 ⊢ (Rel ∅ ↔ ∅ ⊆ (V × V))
3	1, 2	mpbir 234	1 ⊢ Rel ∅

This proof depends on syntax axioms:  Vcvv 3450   ⊆ wss 3896  ∅c0 4277   × cxp 5649  Rel wrel 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3897  df-dif 4046  df-nul 4278  df-rel 5658

This theorem is used by:  relsnb  5781  reldm0  5911  cnveq0  6193  cnveq0b  6194  co02  6265  co01  6266  tpos0  8281  0we1  8522  0er  8764  canthwe  10743  relexpreld  15202  disjALTV0  39923  dibvalrel  42357  dicvalrelN  42379  dihvalrel  42473  reldmprcof1  50652  reldmprcof2  50653  reldmlan2  50936  reldmran2  50937  rellan  50942  relran  50943