Theorem abn0 4379

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

Assertion

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

Proof of Theorem abn0

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1539   = wceq 1541  ∃wex 1781  {cab 2709   ≠ wne 2940  ∅c0 4321

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-ne 2941  df-dif 3950  df-nul 4322

This theorem is referenced by:  intexab  5338  iinexg  5340  relimasn  6080  inisegn0  6094  mapprc  8820  modom  9240  tz9.1c  9721  scott0  9877  scott0s  9879  cp  9882  karden  9886  acnrcl  10033  aceq3lem  10111  cff  10239  cff1  10249  cfss  10256  domtriomlem  10433  axdclem  10510  nqpr  11005  supadd  12178  supmul  12182  hashf1lem2  14413  hashf1  14414  mreiincl  17536  efgval  19579  efger  19580  birthdaylem3  26447  disjex  31810  disjexc  31811  mppsval  34551  mblfinlem3  36515  ismblfin  36517  itg2addnc  36530  sdclem1  36599  upbdrech  44001