Theorem n0i 4315

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-dif 3929  df-nul 4309

This theorem is referenced by:  ne0i  4316  n0ii  4318  oprcl  4875  disjss3  5118  elfvdm  6912  mptrcl  6994  isomin  7329  ovrcl  7444  elfvov1  7445  elfvov2  7446  oalimcl  8570  omlimcl  8588  nnaordex2  8649  oaabs2  8659  ecexr  8722  elpmi  8858  elmapex  8860  pmresg  8882  pmsspw  8889  ixpssmap2g  8939  ixpssmapg  8940  resixpfo  8948  php3  9221  php3OLD  9231  cantnfp1lem2  9691  cantnflem1  9701  cnfcom2lem  9713  rankxplim2  9892  rankxplim3  9893  cardlim  9984  alephnbtwn  10083  ttukeylem5  10525  r1wunlim  10749  ssnn0fi  14001  ruclem13  16258  ramtub  17030  elbasfv  17232  elbasov  17233  restsspw  17443  homarcl  18039  grpidval  18637  odlem2  19518  efgrelexlema  19728  subcmn  19816  dvdsrval  20319  elocv  21626  pf1rcl  22285  matrcl  22348  0top  22919  ppttop  22943  pptbas  22944  restrcl  23093  ssrest  23112  iscnp2  23175  lmmo  23316  zfbas  23832  rnelfmlem  23888  isfcls  23945  isnghm  24660  iscau2  25227  itg2cnlem1  25712  itgsubstlem  26005  dchrrcl  27201  clwwlknnn  29960  0ringsubrg  33192  ssdifidllem  33417  ssmxidllem  33434  eulerpartlemgvv  34354  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  36341  nlpineqsn  37372  atbase  39253  llnbase  39474  lplnbase  39499  lvolbase  39543  osumcllem4N  39924  pexmidlem1N  39935  lhpbase  39963  mapco2g  42684  wepwsolem  43013  onov0suclim  43245  uneqsn  43996  relpmin  44925  ssfiunibd  45286  hoicvr  46525  0nelsetpreimafv  47352  termchomn0  49317