Theorem rel0 5779

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

This proof depends on syntax axioms:  Vcvv 3450   ⊆ wss 3899  ∅c0 4279   × cxp 5653  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-dif 3902  df-ss 3916  df-nul 4280  df-rel 5662

This theorem is used by:  relsnb  5783  reldm0  5912  cnveq0  6191  co02  6257  co01  6258  tpos0  8254  0we1  8493  0er  8735  canthwe  10660  relexpreld  15113  disjALTV0  39602  dibvalrel  42036  dicvalrelN  42058  dihvalrel  42152  reldmprcof1  50307  reldmprcof2  50308  reldmlan2  50543  reldmran2  50544  rellan  50549  relran  50550