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

Syntax hints:  Vcvv 3436   ⊆ wss 3903  ∅c0 4284   × cxp 5617  Rel wrel 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3906  df-ss 3920  df-nul 4285  df-rel 5626

This theorem is referenced by:  relsnb  5745  reldm0  5870  cnveq0  6146  co02  6209  co01  6210  tpos0  8189  0we1  8424  0er  8663  canthwe  10545  relexpreld  14947  disjALTV0  38732  dibvalrel  41142  dicvalrelN  41164  dihvalrel  41258  reldmprcof1  49366  reldmprcof2  49367  reldmlan2  49602  reldmran2  49603  rellan  49608  relran  49609