Theorem rel0 5776

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

This proof depends on syntax axioms:  Vcvv 3451   ⊆ wss 3899  ∅c0 4279   × cxp 5649  Rel wrel 5656

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-dif 3902  df-ss 3916  df-nul 4280  df-rel 5658

This theorem is used by:  relsnb  5780  reldm0  5910  cnveq0  6191  co02  6262  co01  6263  tpos0  8273  0we1  8514  0er  8756  canthwe  10736  relexpreld  15193  disjALTV0  39786  dibvalrel  42220  dicvalrelN  42242  dihvalrel  42336  reldmprcof1  50488  reldmprcof2  50489  reldmlan2  50724  reldmran2  50725  rellan  50730  relran  50731