Theorem ne0i 3308

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

Assertion

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

Proof of Theorem ne0i

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

Syntax hints:   → wi 4   ∈ wcel 1445   ≠ wne 2262  ∅c0 3302

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-v 2635  df-dif 3015  df-nul 3303

This theorem is referenced by:  ne0d  3309  ne0ii  3311  vn0  3312  inelcm  3362  rzal  3399  rexn0  3400  snnzg  3579  prnz  3584  tpnz  3587  onn0  4251  nn0eln0  4461  ordge1n0im  6238  nnmord  6316  map0g  6485  phpm  6661  fiintim  6719  addclpi  6983  mulclpi  6984  uzn0  9133  iccsupr  9532