Theorem abn0 4314

Description: Nonempty class abstraction. See also ab0 4308. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2816, ax-8 2108. (Revised by Gino Giotto, 30-Aug-2024.)

Assertion

Ref	Expression
abn0	⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4308	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2944	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅)
4		df-ex 1783	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537   = wceq 1539  ∃wex 1782  {cab 2715   ≠ wne 2943  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-ne 2944  df-dif 3890  df-nul 4257

This theorem is referenced by:  intexab  5263  iinexg  5265  relimasn  5992  inisegn0  6006  mapprc  8619  modom  9023  tz9.1c  9488  scott0  9644  scott0s  9646  cp  9649  karden  9653  acnrcl  9798  aceq3lem  9876  cff  10004  cff1  10014  cfss  10021  domtriomlem  10198  axdclem  10275  nqpr  10770  supadd  11943  supmul  11947  hashf1lem2  14170  hashf1  14171  mreiincl  17305  efgval  19323  efger  19324  birthdaylem3  26103  disjex  30931  disjexc  30932  mppsval  33534  mblfinlem3  35816  ismblfin  35818  itg2addnc  35831  sdclem1  35901  upbdrech  42844