Theorem abn0 4337

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

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4332	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 323	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2960	. 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 2741   ≠ wne 2959  ∅c0 4281

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-ne 2960  df-dif 4050  df-nul 4282

This theorem is used by:  intexab  5314  iinexg  5316  inisegn0  6114  mapprc  8889  modom  9280  tz9.1c  9768  scott0b  9974  scott0OLD  9975  scott0bs  9981  scott0bsOLD  9982  cp  9991  karden  9996  kardenOLD  9997  acnrcl  10160  aceq3lem  10238  cff  10364  cff1  10375  cfss  10382  domtriomlem  10559  axdclem  10636  nqpr  11138  supadd  12325  supmul  12329  hashf1lem2  14642  hashf1  14643  mreiincl  17816  efgval  19982  efger  19983  birthdaylem3  27338  disjex  33284  disjexc  33285  axregs  35948  kardeq0  35965  mppsval  36545  regsfromunir1  37543  mblfinlem3  38845  ismblfin  38847  itg2addnc  38860  sdclem1  38943  upbdrech  46594