Theorem rel0 5785

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

Syntax hints:  Vcvv 3455   ⊆ wss 3905  ∅c0 4286   × cxp 5659  Rel wrel 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3908  df-ss 3922  df-nul 4287  df-rel 5668

This theorem is referenced by:  relsnb  5789  reldm0  5918  cnveq0  6196  co02  6262  co01  6263  tpos0  8248  0we1  8487  0er  8729  canthwe  10631  relexpreld  15073  disjALTV0  39503  dibvalrel  41937  dicvalrelN  41959  dihvalrel  42053  reldmprcof1  50159  reldmprcof2  50160  reldmlan2  50395  reldmran2  50396  rellan  50401  relran  50402