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 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2146  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-dif 3909  df-nul 4287

This theorem is used by:  ne0i  4294  n0ii  4296  oprcl  4866  disjss3  5110  elfvdm  6919  mptrcl  7003  isomin  7344  ovrcl  7460  elfvov1  7461  elfvov2  7462  oalimcl  8551  omlimcl  8569  nnaordex2  8631  oaabs2  8641  ecexr  8705  elpmi  8849  elmapex  8851  pmresg  8874  pmsspw  8881  ixpssmap2g  8931  ixpssmapg  8932  resixpfo  8940  php3  9200  cantnfp1lem2  9655  cantnflem1  9665  cnfcom2lem  9677  rankxplim2  9859  rankxplim3  9860  cardlim  9974  alephnbtwn  10071  ttukeylem5  10512  r1wunlim  10737  ssnn0fi  14039  ruclem13  16320  ramtub  17094  elbasfv  17297  elbasov  17298  restsspw  17506  homarcl  18107  grpidval  18744  odlem2  19653  efgrelexlema  19863  subcmn  19951  dvdsrval  20489  ssdifidllem  21534  elocv  21868  pf1rcl  22559  matrcl  22619  0top  23190  ppttop  23214  pptbas  23215  restrcl  23364  ssrest  23383  iscnp2  23446  lmmo  23587  zfbas  24104  rnelfmlem  24160  isfcls  24217  isnghm  24931  iscau2  25487  itg2cnlem1  25971  itgsubstlem  26258  dchrrcl  27455  clwwlknnn  30451  0ringsubrg  33635  ssmxidllem  33820  eulerpartlemgvv  34831  indispconn  35763  cvmtop1  35789  cvmtop2  35790  mrsub0  36045  mrsubf  36046  mrsubccat  36047  mrsubcn  36048  mrsubco  36050  mrsubvrs  36051  msubf  36061  mclsrcl  36090  funpartlem  36471  tailfb  36945  nlpineqsn  38111  atbase  40121  llnbase  40341  lplnbase  40366  lvolbase  40410  osumcllem4N  40791  pexmidlem1N  40802  lhpbase  40830  mapco2g  43503  wepwsolem  43827  onov0suclim  44059  uneqsn  44809  relpmin  45719  ssfiunibd  46086  hoicvr  47320  0nelsetpreimafv  48197  termchomn0  50319