Theorem abn0 4332

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

Assertion

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

Proof of Theorem abn0

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539   = wceq 1541  ∃wex 1780  {cab 2709   ≠ wne 2928  ∅c0 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-ne 2929  df-dif 3900  df-nul 4281

This theorem is referenced by:  intexab  5282  iinexg  5284  inisegn0  6046  mapprc  8754  modom  9135  tz9.1c  9620  scott0  9779  scott0s  9781  cp  9784  karden  9788  acnrcl  9933  aceq3lem  10011  cff  10139  cff1  10149  cfss  10156  domtriomlem  10333  axdclem  10410  nqpr  10905  supadd  12090  supmul  12094  hashf1lem2  14363  hashf1  14364  mreiincl  17498  efgval  19629  efger  19630  birthdaylem3  26890  disjex  32572  disjexc  32573  axregs  35145  mppsval  35616  mblfinlem3  37707  ismblfin  37709  itg2addnc  37722  sdclem1  37791  upbdrech  45354