Theorem abn0 4408

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

Assertion

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

Proof of Theorem abn0

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1535   = wceq 1537  ∃wex 1777  {cab 2717   ≠ wne 2946  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-ne 2947  df-dif 3979  df-nul 4353

This theorem is referenced by:  intexab  5364  iinexg  5366  relimasn  6114  inisegn0  6128  mapprc  8888  modom  9307  tz9.1c  9799  scott0  9955  scott0s  9957  cp  9960  karden  9964  acnrcl  10111  aceq3lem  10189  cff  10317  cff1  10327  cfss  10334  domtriomlem  10511  axdclem  10588  nqpr  11083  supadd  12263  supmul  12267  hashf1lem2  14505  hashf1  14506  mreiincl  17654  efgval  19759  efger  19760  birthdaylem3  27014  disjex  32614  disjexc  32615  mppsval  35540  mblfinlem3  37619  ismblfin  37621  itg2addnc  37634  sdclem1  37703  upbdrech  45220