Theorem n0i 4292

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3904  df-nul 4286

This theorem is referenced by:  ne0i  4293  n0ii  4295  oprcl  4855  disjss3  5097  elfvdm  6868  mptrcl  6950  isomin  7283  ovrcl  7399  elfvov1  7400  elfvov2  7401  oalimcl  8487  omlimcl  8505  nnaordex2  8567  oaabs2  8577  ecexr  8640  elpmi  8783  elmapex  8785  pmresg  8808  pmsspw  8815  ixpssmap2g  8865  ixpssmapg  8866  resixpfo  8874  php3  9133  cantnfp1lem2  9588  cantnflem1  9598  cnfcom2lem  9610  rankxplim2  9792  rankxplim3  9793  cardlim  9884  alephnbtwn  9981  ttukeylem5  10423  r1wunlim  10648  ssnn0fi  13908  ruclem13  16167  ramtub  16940  elbasfv  17142  elbasov  17143  restsspw  17351  homarcl  17952  grpidval  18586  odlem2  19468  efgrelexlema  19678  subcmn  19766  dvdsrval  20297  elocv  21623  pf1rcl  22293  matrcl  22356  0top  22927  ppttop  22951  pptbas  22952  restrcl  23101  ssrest  23120  iscnp2  23183  lmmo  23324  zfbas  23840  rnelfmlem  23896  isfcls  23953  isnghm  24667  iscau2  25233  itg2cnlem1  25718  itgsubstlem  26011  dchrrcl  27207  clwwlknnn  30108  0ringsubrg  33333  ssdifidllem  33537  ssmxidllem  33554  eulerpartlemgvv  34533  indispconn  35428  cvmtop1  35454  cvmtop2  35455  mrsub0  35710  mrsubf  35711  mrsubccat  35712  mrsubcn  35713  mrsubco  35715  mrsubvrs  35716  msubf  35726  mclsrcl  35755  funpartlem  36136  tailfb  36571  nlpineqsn  37613  atbase  39549  llnbase  39769  lplnbase  39794  lvolbase  39838  osumcllem4N  40219  pexmidlem1N  40230  lhpbase  40258  mapco2g  42956  wepwsolem  43284  onov0suclim  43516  uneqsn  44266  relpmin  45193  ssfiunibd  45557  hoicvr  46792  0nelsetpreimafv  47636  termchomn0  49729