Theorem rel0 5786

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

Syntax hints:  Vcvv 3463   ⊆ wss 3913  ∅c0 4294   × cxp 5660  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-dif 3916  df-ss 3930  df-nul 4295  df-rel 5669

This theorem is referenced by:  relsnb  5790  reldm0  5919  cnveq0  6197  co02  6263  co01  6264  tpos0  8251  0we1  8490  0er  8732  canthwe  10635  relexpreld  15076  disjALTV0  39392  dibvalrel  41826  dicvalrelN  41848  dihvalrel  41942  reldmprcof1  50043  reldmprcof2  50044  reldmlan2  50279  reldmran2  50280  rellan  50285  relran  50286