Theorem abn0 4337

Description: Nonempty class abstraction. See also ab0 4332. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2811, ax-8 2115. (Revised by GG, 30-Aug-2024.)

Assertion

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

Proof of Theorem abn0

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539   = wceq 1541  ∃wex 1780  {cab 2714   ≠ wne 2932  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-ne 2933  df-dif 3904  df-nul 4286

This theorem is referenced by:  intexab  5291  iinexg  5293  inisegn0  6057  mapprc  8767  modom  9151  tz9.1c  9639  scott0  9798  scott0s  9800  cp  9803  karden  9807  acnrcl  9952  aceq3lem  10030  cff  10158  cff1  10168  cfss  10175  domtriomlem  10352  axdclem  10429  nqpr  10925  supadd  12110  supmul  12114  hashf1lem2  14379  hashf1  14380  mreiincl  17515  efgval  19646  efger  19647  birthdaylem3  26919  disjex  32667  disjexc  32668  axregs  35295  mppsval  35766  regsfromunir1  36670  mblfinlem3  37860  ismblfin  37862  itg2addnc  37875  sdclem1  37944  upbdrech  45553