Theorem 0ss 3406

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 3372	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 636	. 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴)
3	2	ssriv 3106	1 ⊢ ∅ ⊆ 𝐴

Syntax hints:   ∈ wcel 1481   ⊆ wss 3076  ∅c0 3368

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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-dif 3078  df-in 3082  df-ss 3089  df-nul 3369

This theorem is referenced by:  ss0b  3407  ssdifeq0  3450  sssnr  3688  ssprr  3691  uni0  3771  int0el  3809  0disj  3934  disjx0  3936  tr0  4045  0elpw  4096  exmidsssn  4133  fr0  4281  elnn  4527  rel0  4672  0ima  4907  fun0  5189  f0  5321  oaword1  6375  0domg  6739  nnnninf  7031  exmidfodomrlemim  7074  sum0  11189  ennnfonelemj0  11950  ennnfonelemkh  11961  0opn  12212  baspartn  12256  0cld  12320  ntr0  12342  bdeq0  13236  bj-omtrans  13325  el2oss1o  13359  nninfsellemsuc  13383