Theorem abn0 4333

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

Assertion

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

Proof of Theorem abn0

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1567   = wceq 1569  ∃wex 1811  {cab 2738   ≠ wne 2955  ∅c0 4277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-ne 2956  df-dif 4046  df-nul 4278

This theorem is used by:  intexab  5307  iinexg  5309  inisegn0  6098  mapprc  8859  modom  9250  tz9.1c  9738  scott0b  9944  scott0OLD  9945  scott0bs  9951  scott0bsOLD  9952  cp  9961  karden  9966  kardenOLD  9967  acnrcl  10128  aceq3lem  10206  cff  10332  cff1  10343  cfss  10350  domtriomlem  10527  axdclem  10604  nqpr  11106  supadd  12292  supmul  12296  hashf1lem2  14608  hashf1  14609  mreiincl  17775  efgval  19940  efger  19941  birthdaylem3  27290  disjex  33237  disjexc  33238  axregs  35875  kardeq0  35892  mppsval  36455  regsfromunir1  37452  mblfinlem3  38714  ismblfin  38716  itg2addnc  38729  sdclem1  38814  upbdrech  46457