Theorem abn0 4335

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

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4330	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2931	. 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 2712   ≠ wne 2930  ∅c0 4283

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 2182  ax-ext 2706

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 2713  df-cleq 2726  df-ne 2931  df-dif 3902  df-nul 4284

This theorem is referenced by:  intexab  5289  iinexg  5291  inisegn0  6055  mapprc  8765  modom  9149  tz9.1c  9637  scott0  9796  scott0s  9798  cp  9801  karden  9805  acnrcl  9950  aceq3lem  10028  cff  10156  cff1  10166  cfss  10173  domtriomlem  10350  axdclem  10427  nqpr  10923  supadd  12108  supmul  12112  hashf1lem2  14377  hashf1  14378  mreiincl  17513  efgval  19644  efger  19645  birthdaylem3  26917  disjex  32616  disjexc  32617  axregs  35244  mppsval  35715  mblfinlem3  37799  ismblfin  37801  itg2addnc  37814  sdclem1  37883  upbdrech  45495