Theorem abn0 4351

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

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4346	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2927	. 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 2708   ≠ wne 2926  ∅c0 4299

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 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-ne 2927  df-dif 3920  df-nul 4300

This theorem is referenced by:  intexab  5304  iinexg  5306  relimasn  6059  inisegn0  6072  mapprc  8806  modom  9198  tz9.1c  9690  scott0  9846  scott0s  9848  cp  9851  karden  9855  acnrcl  10002  aceq3lem  10080  cff  10208  cff1  10218  cfss  10225  domtriomlem  10402  axdclem  10479  nqpr  10974  supadd  12158  supmul  12162  hashf1lem2  14428  hashf1  14429  mreiincl  17564  efgval  19654  efger  19655  birthdaylem3  26870  disjex  32528  disjexc  32529  mppsval  35566  mblfinlem3  37660  ismblfin  37662  itg2addnc  37675  sdclem1  37744  upbdrech  45310