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 2840, ax-8 2148. (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 2961	. 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 2743   ≠ wne 2960  ∅c0 4286

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-ne 2961  df-dif 3909  df-nul 4287

This theorem is used by:  intexab  5318  iinexg  5320  inisegn0  6102  mapprc  8834  modom  9218  tz9.1c  9706  scott0b  9873  scott0OLD  9874  scott0bs  9880  scott0bsOLD  9881  cp  9890  karden  9895  kardenOLD  9896  acnrcl  10042  aceq3lem  10120  cff  10246  cff1  10257  cfss  10264  domtriomlem  10441  axdclem  10518  nqpr  11014  supadd  12198  supmul  12202  hashf1lem2  14511  hashf1  14512  mreiincl  17670  efgval  19831  efger  19832  birthdaylem3  27169  disjex  33008  disjexc  33009  axregs  35609  kardeq0  35626  mppsval  36101  regsfromunir1  37108  mblfinlem3  38367  ismblfin  38369  itg2addnc  38382  sdclem1  38452  upbdrech  46082