Theorem abn0 4391

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

Assertion

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

Proof of Theorem abn0

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1535   = wceq 1537  ∃wex 1776  {cab 2712   ≠ wne 2938  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-ne 2939  df-dif 3966  df-nul 4340

This theorem is referenced by:  intexab  5352  iinexg  5354  relimasn  6105  inisegn0  6119  mapprc  8869  modom  9278  tz9.1c  9768  scott0  9924  scott0s  9926  cp  9929  karden  9933  acnrcl  10080  aceq3lem  10158  cff  10286  cff1  10296  cfss  10303  domtriomlem  10480  axdclem  10557  nqpr  11052  supadd  12234  supmul  12238  hashf1lem2  14492  hashf1  14493  mreiincl  17641  efgval  19750  efger  19751  birthdaylem3  27011  disjex  32612  disjexc  32613  mppsval  35557  mblfinlem3  37646  ismblfin  37648  itg2addnc  37661  sdclem1  37730  upbdrech  45256