Theorem abn0 4326

Description: Nonempty class abstraction. See also ab0 4321. (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 4321	. . 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 4274

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 3893  df-nul 4275

This theorem is referenced by:  intexab  5284  iinexg  5286  inisegn0  6058  mapprc  8771  modom  9155  tz9.1c  9645  scott0  9804  scott0s  9806  cp  9809  karden  9813  acnrcl  9958  aceq3lem  10036  cff  10164  cff1  10174  cfss  10181  domtriomlem  10358  axdclem  10435  nqpr  10931  supadd  12118  supmul  12122  hashf1lem2  14412  hashf1  14413  mreiincl  17552  efgval  19686  efger  19687  birthdaylem3  26933  disjex  32680  disjexc  32681  axregs  35302  mppsval  35773  regsfromunir1  36741  mblfinlem3  37997  ismblfin  37999  itg2addnc  38012  sdclem1  38081  upbdrech  45759