Theorem 0ss 3453

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	⊢ ∅ ⊆ 𝐴

Proof of Theorem 0ss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 3418	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 641	. 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴)
3	2	ssriv 3151	1 ⊢ ∅ ⊆ 𝐴

Syntax hints:   ∈ wcel 2141   ⊆ wss 3121  ∅c0 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123  df-in 3127  df-ss 3134  df-nul 3415

This theorem is referenced by:  ss0b  3454  ssdifeq0  3497  sssnr  3740  ssprr  3743  uni0  3823  int0el  3861  0disj  3986  disjx0  3988  tr0  4098  0elpw  4150  exmidsssn  4188  fr0  4336  elomssom  4589  rel0  4736  0ima  4971  fun0  5256  f0  5388  el2oss1o  6422  oaword1  6450  0domg  6815  nnnninf  7102  exmidfodomrlemim  7178  pw1on  7203  sum0  11351  prod0  11548  ennnfonelemj0  12356  ennnfonelemkh  12367  0opn  12798  baspartn  12842  0cld  12906  ntr0  12928  bdeq0  13902  bj-omtrans  13991  nninfsellemsuc  14045