Theorem n0i 4264

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		noel 4261	. . 3 ⊢ ¬ 𝐵 ∈ ∅
2		eleq2 2827	. . 3 ⊢ (𝐴 = ∅ → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ ∅))
3	1, 2	mtbiri 326	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
4	3	con2i 139	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2108  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-dif 3886  df-nul 4254

This theorem is referenced by:  ne0i  4265  n0ii  4267  oprcl  4827  disjss3  5069  elfvdm  6788  mptrcl  6866  isomin  7188  ovrcl  7296  oalimcl  8353  omlimcl  8371  oaabs2  8439  ecexr  8461  elpmi  8592  elmapex  8594  pmresg  8616  pmsspw  8623  ixpssmap2g  8673  ixpssmapg  8674  resixpfo  8682  php3  8899  cantnfp1lem2  9367  cantnflem1  9377  cnfcom2lem  9389  rankxplim2  9569  rankxplim3  9570  cardlim  9661  alephnbtwn  9758  ttukeylem5  10200  r1wunlim  10424  ssnn0fi  13633  ruclem13  15879  ramtub  16641  elbasfv  16846  elbasov  16847  restsspw  17059  homarcl  17659  grpidval  18260  odlem2  19062  efgrelexlema  19270  subcmn  19353  dvdsrval  19802  elocv  20785  pf1rcl  21425  matrcl  21469  0top  22041  ppttop  22065  pptbas  22066  restrcl  22216  ssrest  22235  iscnp2  22298  lmmo  22439  zfbas  22955  rnelfmlem  23011  isfcls  23068  isnghm  23793  iscau2  24346  itg2cnlem1  24831  itgsubstlem  25117  dchrrcl  26293  clwwlknnn  28298  ssmxidllem  31543  eulerpartlemgvv  32243  indispconn  33096  cvmtop1  33122  cvmtop2  33123  mrsub0  33378  mrsubf  33379  mrsubccat  33380  mrsubcn  33381  mrsubco  33383  mrsubvrs  33384  msubf  33394  mclsrcl  33423  funpartlem  34171  tailfb  34493  nlpineqsn  35506  atbase  37230  llnbase  37450  lplnbase  37475  lvolbase  37519  osumcllem4N  37900  pexmidlem1N  37911  lhpbase  37939  mapco2g  40452  wepwsolem  40783  uneqsn  41522  ssfiunibd  42738  hoicvr  43976  0nelsetpreimafv  44730