Theorem abn0 4341

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

Assertion

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

Proof of Theorem abn0

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1809  {cab 2741   ≠ wne 2958  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-ne 2959  df-dif 3908  df-nul 4287

This theorem is referenced by:  intexab  5316  iinexg  5318  inisegn0  6100  mapprc  8824  modom  9207  tz9.1c  9695  scott0  9856  scott0s  9858  cp  9873  karden  9877  acnrcl  10022  aceq3lem  10100  cff  10226  cff1  10237  cfss  10244  domtriomlem  10421  axdclem  10498  nqpr  10994  supadd  12178  supmul  12182  hashf1lem2  14489  hashf1  14490  mreiincl  17643  efgval  19782  efger  19783  birthdaylem3  27118  disjex  32937  disjexc  32938  axregs  35552  kardeq0  35569  mppsval  36064  regsfromunir1  37051  mblfinlem3  38310  ismblfin  38312  itg2addnc  38325  sdclem1  38394  upbdrech  46024