Theorem n0i 4363

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-dif 3979  df-nul 4353

This theorem is referenced by:  ne0i  4364  n0ii  4366  oprcl  4923  disjss3  5165  elfvdm  6957  mptrcl  7038  isomin  7373  ovrcl  7489  elfvov1  7490  elfvov2  7491  oalimcl  8616  omlimcl  8634  nnaordex2  8695  oaabs2  8705  ecexr  8768  elpmi  8904  elmapex  8906  pmresg  8928  pmsspw  8935  ixpssmap2g  8985  ixpssmapg  8986  resixpfo  8994  php3  9275  php3OLD  9287  cantnfp1lem2  9748  cantnflem1  9758  cnfcom2lem  9770  rankxplim2  9949  rankxplim3  9950  cardlim  10041  alephnbtwn  10140  ttukeylem5  10582  r1wunlim  10806  ssnn0fi  14036  ruclem13  16290  ramtub  17059  elbasfv  17264  elbasov  17265  restsspw  17491  homarcl  18095  grpidval  18699  odlem2  19581  efgrelexlema  19791  subcmn  19879  dvdsrval  20387  elocv  21709  pf1rcl  22374  matrcl  22437  0top  23011  ppttop  23035  pptbas  23036  restrcl  23186  ssrest  23205  iscnp2  23268  lmmo  23409  zfbas  23925  rnelfmlem  23981  isfcls  24038  isnghm  24765  iscau2  25330  itg2cnlem1  25816  itgsubstlem  26109  dchrrcl  27302  clwwlknnn  30065  0ringsubrg  33223  ssdifidllem  33449  ssmxidllem  33466  eulerpartlemgvv  34341  indispconn  35202  cvmtop1  35228  cvmtop2  35229  mrsub0  35484  mrsubf  35485  mrsubccat  35486  mrsubcn  35487  mrsubco  35489  mrsubvrs  35490  msubf  35500  mclsrcl  35529  funpartlem  35906  tailfb  36343  nlpineqsn  37374  atbase  39245  llnbase  39466  lplnbase  39491  lvolbase  39535  osumcllem4N  39916  pexmidlem1N  39927  lhpbase  39955  mapco2g  42670  wepwsolem  42999  onov0suclim  43236  uneqsn  43987  ssfiunibd  45224  hoicvr  46469  0nelsetpreimafv  47264