Theorem abn0 4338

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

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4333	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 322	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2958	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅)
4		df-ex 1800	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 305	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1558   = wceq 1560  ∃wex 1799  {cab 2740   ≠ wne 2957  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-ne 2958  df-dif 3907  df-nul 4286

This theorem is referenced by:  intexab  5302  iinexg  5304  inisegn0  6087  mapprc  8812  modom  9195  tz9.1c  9685  scott0  9844  scott0s  9846  cp  9849  karden  9853  acnrcl  9998  aceq3lem  10076  cff  10204  cff1  10215  cfss  10222  domtriomlem  10399  axdclem  10476  nqpr  10972  supadd  12160  supmul  12164  hashf1lem2  14469  hashf1  14470  mreiincl  17624  efgval  19757  efger  19758  birthdaylem3  27015  disjex  32789  disjexc  32790  axregs  35432  mppsval  35919  regsfromunir1  36897  mblfinlem3  38155  ismblfin  38157  itg2addnc  38170  sdclem1  38239  upbdrech  45881