Theorem ne0i 3501

Description: If a set has elements, it is not empty. A set with elements is also inhabited, see elex2 2819. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
ne0i	⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

Proof of Theorem ne0i

Step	Hyp	Ref	Expression
1		n0i 3500	. 2 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
2	1	neneqad 2481	1 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2202   ≠ wne 2402  ∅c0 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-v 2804  df-dif 3202  df-nul 3495

This theorem is referenced by:  ne0d  3502  ne0ii  3504  vn0  3505  inelcm  3555  rzal  3592  rexn0  3593  snnzg  3789  prnz  3795  tpnz  3798  brne0  4138  onn0  4497  nn0eln0  4718  ordge1n0im  6603  nnmord  6684  map0g  6856  phpm  7051  fiintim  7122  addclpi  7546  mulclpi  7547  uzn0  9771  iccsupr  10200  pfxn0  11268  ringn0  14072