Theorem abn0 4336

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

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4331	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2926	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅)
4		df-ex 1780	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538   = wceq 1540  ∃wex 1779  {cab 2707   ≠ wne 2925  ∅c0 4284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-ne 2926  df-dif 3906  df-nul 4285

This theorem is referenced by:  intexab  5285  iinexg  5287  relimasn  6036  inisegn0  6049  mapprc  8757  modom  9140  tz9.1c  9626  scott0  9782  scott0s  9784  cp  9787  karden  9791  acnrcl  9936  aceq3lem  10014  cff  10142  cff1  10152  cfss  10159  domtriomlem  10336  axdclem  10413  nqpr  10908  supadd  12093  supmul  12097  hashf1lem2  14363  hashf1  14364  mreiincl  17498  efgval  19596  efger  19597  birthdaylem3  26861  disjex  32536  disjexc  32537  axregs  35074  mppsval  35545  mblfinlem3  37639  ismblfin  37641  itg2addnc  37654  sdclem1  37723  upbdrech  45287