Theorem abn0 4313

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

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4308	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 321	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2935	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅)
4		df-ex 1787	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 304	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wal 1545   = wceq 1547  ∃wex 1786  {cab 2717   ≠ wne 2934  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-ne 2935  df-dif 3886  df-nul 4262

This theorem is referenced by:  intexab  5274  iinexg  5276  inisegn0  6050  mapprc  8767  modom  9151  tz9.1c  9642  scott0  9801  scott0s  9803  cp  9806  karden  9810  acnrcl  9955  aceq3lem  10033  cff  10161  cff1  10171  cfss  10178  domtriomlem  10355  axdclem  10432  nqpr  10928  supadd  12115  supmul  12119  hashf1lem2  14409  hashf1  14410  mreiincl  17549  efgval  19683  efger  19684  birthdaylem3  26935  disjex  32681  disjexc  32682  axregs  35320  mppsval  35800  regsfromunir1  36768  mblfinlem3  38026  ismblfin  38028  itg2addnc  38041  sdclem1  38110  upbdrech  45753