Theorem neq0 4287

Description: A class is not empty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 21-Jun-1993.) Avoid ax-11 2168, ax-12 2189. (Revised by GG, 28-Jun-2024.)

Assertion

Ref	Expression
neq0	⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

Step	Hyp	Ref	Expression
1		df-ex 1787	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4285	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 336	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 225	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wal 1545   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-dif 3893  df-nul 4269

This theorem is referenced by:  n0  4288  falseral0OLD  4450  snprc  4656  pwpw0  4751  sssn  4764  uni0b  4871  disjor  5061  rnep  5876  isomin  7288  mpoxneldm  8159  mpoxopynvov0g  8161  mpoxopxnop0  8162  erdisj  8698  ixpprc  8864  domunsn  9062  sucdom2  9134  isinf  9172  nfielex  9181  scottex  9807  acndom  9971  axcclem  10377  axpowndlem3  10520  canthp1lem1  10573  isumltss  15811  nzerooringczr  21462  pf1rcl  22342  ppttop  22997  ntreq0  23067  txindis  23624  txconn  23679  fmfnfm  23948  ptcmplem2  24043  ptcmplem3  24044  bddmulibl  25831  g0wlk0  29744  wwlksnndef  29998  strlem1  32346  disjorf  32675  ssdifidlprm  33548  1arithufdlem4  33637  ddemeas  34427  tgoldbachgt  34854  bnj1143  34979  prv1n  35666  pibt2  37786  poimirlem25  38019  poimirlem27  38021  ineleq  38728  dmcnvep  38762  eqvreldisj  39072  grucollcld  44711  relpmin  45403  fnchoice  45484  founiiun0  45644  mo0sn  49313  map0cor  49352  termchom  49985