Theorem n0i 3879

Description: If a set 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 3878	. . 3 ⊢ ¬ 𝐵 ∈ ∅
2		eleq2 2677	. . 3 ⊢ (𝐴 = ∅ → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ ∅))
3	1, 2	mtbiri 316	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
4	3	con2i 133	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ∈ wcel 1977  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  ne0i  3880  n0ii  3881  oprcl  4365  disjss3  4582  mptrcl  6198  isomin  6487  ovrcl  6584  oalimcl  7527  omlimcl  7545  oaabs2  7612  ecexr  7634  elpmi  7762  elmapex  7764  pmresg  7771  pmsspw  7778  ixpssmap2g  7823  ixpssmapg  7824  resixpfo  7832  php3  8031  cantnfp1lem2  8459  cantnflem1  8469  cnfcom2lem  8481  rankxplim2  8626  rankxplim3  8627  cardlim  8681  alephnbtwn  8777  ttukeylem5  9218  r1wunlim  9438  ssnn0fi  12646  ruclem13  14810  ramtub  15554  elbasfv  15748  elbasov  15749  restsspw  15915  homarcl  16501  grpidval  17083  odlem2  17781  efgrelexlema  17985  subcmn  18065  dvdsrval  18468  pf1rcl  19534  elocv  19831  matrcl  20037  0top  20598  ppttop  20621  pptbas  20622  restrcl  20771  ssrest  20790  iscnp2  20853  lmmo  20994  zfbas  21510  rnelfmlem  21566  isfcls  21623  isnghm  22337  iscau2  22883  itg2cnlem1  23334  itgsubstlem  23615  dchrrcl  24765  eleenn  25576  nbgranself2  25965  uvtxisvtx  26018  uvtx01vtx  26020  2spot0  26591  eulerpartlemgvv  29765  indispcon  30470  cvmtop1  30496  cvmtop2  30497  mrsub0  30667  mrsubf  30668  mrsubccat  30669  mrsubcn  30670  mrsubco  30672  mrsubvrs  30673  msubf  30683  mclsrcl  30712  funpartlem  31219  tailfb  31542  atbase  33594  llnbase  33813  lplnbase  33838  lvolbase  33882  osumcllem4N  34263  pexmidlem1N  34274  lhpbase  34302  mapco2g  36295  wepwsolem  36630  uneqsn  37341  ssfiunibd  38464  hoicvr  39438