Theorem abn0 4348

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

Assertion

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

Proof of Theorem abn0

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

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 2701

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 2708  df-cleq 2721  df-ne 2926  df-dif 3917  df-nul 4297

This theorem is referenced by:  intexab  5301  iinexg  5303  relimasn  6056  inisegn0  6069  mapprc  8803  modom  9191  tz9.1c  9683  scott0  9839  scott0s  9841  cp  9844  karden  9848  acnrcl  9995  aceq3lem  10073  cff  10201  cff1  10211  cfss  10218  domtriomlem  10395  axdclem  10472  nqpr  10967  supadd  12151  supmul  12155  hashf1lem2  14421  hashf1  14422  mreiincl  17557  efgval  19647  efger  19648  birthdaylem3  26863  disjex  32521  disjexc  32522  mppsval  35559  mblfinlem3  37653  ismblfin  37655  itg2addnc  37668  sdclem1  37737  upbdrech  45303