Theorem abn0 4348

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

Assertion

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

Proof of Theorem abn0

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1565   = wceq 1567  ∃wex 1806  {cab 2747   ≠ wne 2964  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-ne 2965  df-dif 3916  df-nul 4295

This theorem is referenced by:  intexab  5317  iinexg  5319  inisegn0  6101  mapprc  8827  modom  9210  tz9.1c  9698  scott0  9859  scott0s  9861  cp  9876  karden  9880  acnrcl  10025  aceq3lem  10103  cff  10230  cff1  10241  cfss  10248  domtriomlem  10425  axdclem  10502  nqpr  10998  supadd  12182  supmul  12186  hashf1lem2  14492  hashf1  14493  mreiincl  17647  efgval  19786  efger  19787  birthdaylem3  27083  disjex  32877  disjexc  32878  axregs  35474  mppsval  35962  regsfromunir1  36939  mblfinlem3  38197  ismblfin  38199  itg2addnc  38212  sdclem1  38281  upbdrech  45915