Theorem 0ex 4110

Description: The empty class exists. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
0ex	⊢ ∅ ∈ V

Proof of Theorem 0ex

Step	Hyp	Ref	Expression
1		complV 4070	. 2 ⊢ ∼ V = ∅
2		vvex 4109	. . 3 ⊢ V ∈ V
3	2	complex 4104	. 2 ⊢ ∼ V ∈ V
4	1, 3	eqeltrri 2424	1 ⊢ ∅ ∈ V

Syntax hints:   ∈ wcel 1710  Vcvv 2859   ∼ ccompl 3205  ∅c0 3550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551

This theorem is referenced by:  snex  4111  setswithex  4322  abexv  4324  iotaex  4356  0cnsuc  4401  addcid1  4405  el0c  4421  preaddccan2lem1  4454  tfinex  4485  0ceven  4505  nnadjoin  4520  nnpweq  4523  sfin01  4528  tfinnn  4534  vfin1cltv  4547  xpexr  5109  fnfullfun  5858  fvfullfun  5864  clos10  5887  po0  5939  connex0  5940  map0e  6023  map0b  6024  map0  6025  en0  6042  endisj  6051  enpw  6087  0cnc  6138  muc0  6142  ncaddccl  6144  1p1e2c  6155  2p1e3c  6156  tcdi  6164  tc1c  6165  ce0nnul  6177  ce0addcnnul  6179  ce0nn  6180  ce0nulnc  6184  ce0  6190  ce2  6192  lec0cg  6198  0lt1c  6258