Theorem abn0 4339

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

Assertion

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

Proof of Theorem abn0

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540   = wceq 1542  ∃wex 1781  {cab 2715   ≠ wne 2933  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-ne 2934  df-dif 3906  df-nul 4288

This theorem is referenced by:  intexab  5293  iinexg  5295  inisegn0  6065  mapprc  8779  modom  9163  tz9.1c  9651  scott0  9810  scott0s  9812  cp  9815  karden  9819  acnrcl  9964  aceq3lem  10042  cff  10170  cff1  10180  cfss  10187  domtriomlem  10364  axdclem  10441  nqpr  10937  supadd  12122  supmul  12126  hashf1lem2  14391  hashf1  14392  mreiincl  17527  efgval  19658  efger  19659  birthdaylem3  26931  disjex  32679  disjexc  32680  axregs  35317  mppsval  35788  regsfromunir1  36692  mblfinlem3  37910  ismblfin  37912  itg2addnc  37925  sdclem1  37994  upbdrech  45667