Theorem abn0 4344

Description: Nonempty class abstraction. See also ab0 4339. (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 4339	. . 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 4292

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 3914  df-nul 4293

This theorem is referenced by:  intexab  5296  iinexg  5298  relimasn  6045  inisegn0  6058  mapprc  8780  modom  9167  tz9.1c  9659  scott0  9815  scott0s  9817  cp  9820  karden  9824  acnrcl  9971  aceq3lem  10049  cff  10177  cff1  10187  cfss  10194  domtriomlem  10371  axdclem  10448  nqpr  10943  supadd  12127  supmul  12131  hashf1lem2  14397  hashf1  14398  mreiincl  17533  efgval  19623  efger  19624  birthdaylem3  26839  disjex  32494  disjexc  32495  mppsval  35532  mblfinlem3  37626  ismblfin  37628  itg2addnc  37641  sdclem1  37710  upbdrech  45276