Theorem n0i 4293

Description: If a class has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
n0i	⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Proof of Theorem n0i

Step	Hyp	Ref	Expression
1		nel02 4292	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
2	1	con2i 140	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2143  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3908  df-nul 4287

This theorem is referenced by:  ne0i  4294  n0ii  4296  oprcl  4864  disjss3  5108  elfvdm  6915  mptrcl  6999  isomin  7335  ovrcl  7451  elfvov1  7452  elfvov2  7453  oalimcl  8541  omlimcl  8559  nnaordex2  8621  oaabs2  8631  ecexr  8695  elpmi  8839  elmapex  8841  pmresg  8864  pmsspw  8871  ixpssmap2g  8921  ixpssmapg  8922  resixpfo  8930  php3  9189  cantnfp1lem2  9644  cantnflem1  9654  cnfcom2lem  9666  rankxplim2  9848  rankxplim3  9849  cardlim  9954  alephnbtwn  10051  ttukeylem5  10492  r1wunlim  10717  ssnn0fi  14017  ruclem13  16293  ramtub  17067  elbasfv  17270  elbasov  17271  restsspw  17479  homarcl  18080  grpidval  18714  odlem2  19604  efgrelexlema  19814  subcmn  19902  dvdsrval  20439  ssdifidllem  21484  elocv  21818  pf1rcl  22509  matrcl  22569  0top  23140  ppttop  23164  pptbas  23165  restrcl  23314  ssrest  23333  iscnp2  23396  lmmo  23537  zfbas  24053  rnelfmlem  24109  isfcls  24166  isnghm  24880  iscau2  25436  itg2cnlem1  25920  itgsubstlem  26207  dchrrcl  27404  clwwlknnn  30384  0ringsubrg  33571  ssmxidllem  33756  eulerpartlemgvv  34766  indispconn  35726  cvmtop1  35752  cvmtop2  35753  mrsub0  36008  mrsubf  36009  mrsubccat  36010  mrsubcn  36011  mrsubco  36013  mrsubvrs  36014  msubf  36024  mclsrcl  36053  funpartlem  36434  tailfb  36888  nlpineqsn  38054  atbase  40063  llnbase  40283  lplnbase  40308  lvolbase  40352  osumcllem4N  40733  pexmidlem1N  40744  lhpbase  40772  mapco2g  43445  wepwsolem  43769  onov0suclim  44001  uneqsn  44751  relpmin  45661  ssfiunibd  46028  hoicvr  47262  0nelsetpreimafv  48139  termchomn0  50262