Theorem rel0 5749

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

Syntax hints:  Vcvv 3430   ⊆ wss 3890  ∅c0 4274   × cxp 5623  Rel wrel 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3893  df-ss 3907  df-nul 4275  df-rel 5632

This theorem is referenced by:  relsnb  5752  reldm0  5878  cnveq0  6156  co02  6220  co01  6221  tpos0  8200  0we1  8435  0er  8676  canthwe  10568  relexpreld  14996  disjALTV0  39192  dibvalrel  41626  dicvalrelN  41648  dihvalrel  41742  reldmprcof1  49871  reldmprcof2  49872  reldmlan2  50107  reldmran2  50108  rellan  50113  relran  50114