Theorem abn0 4311

Description: Nonempty class abstraction. See also ab0 4305. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2817, ax-8 2110. (Revised by Gino Giotto, 30-Aug-2024.)

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4305	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 319	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2943	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅)
4		df-ex 1784	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 302	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537   = wceq 1539  ∃wex 1783  {cab 2715   ≠ wne 2942  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-ne 2943  df-dif 3886  df-nul 4254

This theorem is referenced by:  intexab  5258  iinexg  5260  relimasn  5981  inisegn0  5995  mapprc  8577  modom  8953  tz9.1c  9419  scott0  9575  scott0s  9577  cp  9580  karden  9584  acnrcl  9729  aceq3lem  9807  cff  9935  cff1  9945  cfss  9952  domtriomlem  10129  axdclem  10206  nqpr  10701  supadd  11873  supmul  11877  hashf1lem2  14098  hashf1  14099  mreiincl  17222  efgval  19238  efger  19239  birthdaylem3  26008  disjex  30832  disjexc  30833  mppsval  33434  mblfinlem3  35743  ismblfin  35745  itg2addnc  35758  sdclem1  35828  upbdrech  42734