Theorem rel0 5762

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

Syntax hints:  Vcvv 3447   ⊆ wss 3914  ∅c0 4296   × cxp 5636  Rel wrel 5643

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 3917  df-ss 3931  df-nul 4297  df-rel 5645

This theorem is referenced by:  relsnb  5765  reldm0  5891  cnveq0  6170  co02  6233  co01  6234  tpos0  8235  0we1  8470  0er  8709  canthwe  10604  relexpreld  15006  disjALTV0  38746  dibvalrel  41157  dicvalrelN  41179  dihvalrel  41273  reldmprcof1  49370  reldmprcof2  49371  reldmlan2  49606  reldmran2  49607  rellan  49612  relran  49613