Theorem abn0 4325

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

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4320	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2933	. 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 2714   ≠ wne 2932  ∅c0 4273

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 2708

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 2715  df-cleq 2728  df-ne 2933  df-dif 3892  df-nul 4274

This theorem is referenced by:  intexab  5287  iinexg  5289  inisegn0  6063  mapprc  8777  modom  9161  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  12124  supmul  12128  hashf1lem2  14418  hashf1  14419  mreiincl  17558  efgval  19692  efger  19693  birthdaylem3  26917  disjex  32662  disjexc  32663  axregs  35283  mppsval  35754  regsfromunir1  36722  mblfinlem3  37980  ismblfin  37982  itg2addnc  37995  sdclem1  38064  upbdrech  45738