Theorem abn0 4385

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

Assertion

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

Proof of Theorem abn0

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538   = wceq 1540  ∃wex 1779  {cab 2714   ≠ wne 2940  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-ne 2941  df-dif 3954  df-nul 4334

This theorem is referenced by:  intexab  5346  iinexg  5348  relimasn  6103  inisegn0  6116  mapprc  8870  modom  9280  tz9.1c  9770  scott0  9926  scott0s  9928  cp  9931  karden  9935  acnrcl  10082  aceq3lem  10160  cff  10288  cff1  10298  cfss  10305  domtriomlem  10482  axdclem  10559  nqpr  11054  supadd  12236  supmul  12240  hashf1lem2  14495  hashf1  14496  mreiincl  17639  efgval  19735  efger  19736  birthdaylem3  26996  disjex  32605  disjexc  32606  mppsval  35577  mblfinlem3  37666  ismblfin  37668  itg2addnc  37681  sdclem1  37750  upbdrech  45317