ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0ss Structured version   GIF version

Theorem 0ss 3249
Description: The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
0ss ∅ ⊆ A

Proof of Theorem 0ss
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 noel 3222 . . 3 ¬ x
21pm2.21i 574 . 2 (x ∅ → x A)
32ssriv 2943 1 ∅ ⊆ A
Colors of variables: wff set class
Syntax hints:   wcel 1390  wss 2911  c0 3218
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-dif 2914  df-in 2918  df-ss 2925  df-nul 3219
This theorem is referenced by:  ss0b  3250  0pss  3259  npss0  3260  ssdifeq0  3299  sssnr  3515  ssprr  3518  uni0  3598  int0el  3636  0disj  3752  disjx0  3754  tr0  3856  0elpw  3908  elnn  4271  rel0  4405  0ima  4628  fun0  4900  f0  5023  oaword1  5989  bdeq0  9302  bj-omtrans  9390
  Copyright terms: Public domain W3C validator