Theorem abn0 4334

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

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4329	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 323	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2957	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅)
4		df-ex 1813	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 306	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1812  {cab 2739   ≠ wne 2956  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-ne 2957  df-dif 3902  df-nul 4280

This theorem is used by:  intexab  5307  iinexg  5309  inisegn0  6096  mapprc  8844  modom  9235  tz9.1c  9724  scott0b  9930  scott0OLD  9931  scott0bs  9937  scott0bsOLD  9938  cp  9947  karden  9952  kardenOLD  9953  acnrcl  10114  aceq3lem  10192  cff  10318  cff1  10329  cfss  10336  domtriomlem  10513  axdclem  10590  nqpr  11092  supadd  12278  supmul  12282  hashf1lem2  14594  hashf1  14595  mreiincl  17759  efgval  19924  efger  19925  birthdaylem3  27274  disjex  33179  disjexc  33180  axregs  35790  kardeq0  35807  mppsval  36316  regsfromunir1  37308  mblfinlem3  38557  ismblfin  38559  itg2addnc  38572  sdclem1  38657  upbdrech  46290