Theorem n0i 4306

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-dif 3920  df-nul 4300

This theorem is referenced by:  ne0i  4307  n0ii  4309  oprcl  4866  disjss3  5109  elfvdm  6898  mptrcl  6980  isomin  7315  ovrcl  7431  elfvov1  7432  elfvov2  7433  oalimcl  8527  omlimcl  8545  nnaordex2  8606  oaabs2  8616  ecexr  8679  elpmi  8822  elmapex  8824  pmresg  8846  pmsspw  8853  ixpssmap2g  8903  ixpssmapg  8904  resixpfo  8912  php3  9179  cantnfp1lem2  9639  cantnflem1  9649  cnfcom2lem  9661  rankxplim2  9840  rankxplim3  9841  cardlim  9932  alephnbtwn  10031  ttukeylem5  10473  r1wunlim  10697  ssnn0fi  13957  ruclem13  16217  ramtub  16990  elbasfv  17192  elbasov  17193  restsspw  17401  homarcl  17997  grpidval  18595  odlem2  19476  efgrelexlema  19686  subcmn  19774  dvdsrval  20277  elocv  21584  pf1rcl  22243  matrcl  22306  0top  22877  ppttop  22901  pptbas  22902  restrcl  23051  ssrest  23070  iscnp2  23133  lmmo  23274  zfbas  23790  rnelfmlem  23846  isfcls  23903  isnghm  24618  iscau2  25184  itg2cnlem1  25669  itgsubstlem  25962  dchrrcl  27158  clwwlknnn  29969  0ringsubrg  33209  ssdifidllem  33434  ssmxidllem  33451  eulerpartlemgvv  34374  indispconn  35228  cvmtop1  35254  cvmtop2  35255  mrsub0  35510  mrsubf  35511  mrsubccat  35512  mrsubcn  35513  mrsubco  35515  mrsubvrs  35516  msubf  35526  mclsrcl  35555  funpartlem  35937  tailfb  36372  nlpineqsn  37403  atbase  39289  llnbase  39510  lplnbase  39535  lvolbase  39579  osumcllem4N  39960  pexmidlem1N  39971  lhpbase  39999  mapco2g  42709  wepwsolem  43038  onov0suclim  43270  uneqsn  44021  relpmin  44949  ssfiunibd  45314  hoicvr  46553  0nelsetpreimafv  47395  termchomn0  49477