Theorem abn0 4379

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

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4373	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 319	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2931	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅)
4		df-ex 1775	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 302	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1532   = wceq 1534  ∃wex 1774  {cab 2703   ≠ wne 2930  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-ne 2931  df-dif 3950  df-nul 4324

This theorem is referenced by:  intexab  5337  iinexg  5339  relimasn  6085  inisegn0  6099  mapprc  8849  modom  9269  tz9.1c  9764  scott0  9920  scott0s  9922  cp  9925  karden  9929  acnrcl  10076  aceq3lem  10154  cff  10280  cff1  10290  cfss  10297  domtriomlem  10474  axdclem  10551  nqpr  11046  supadd  12226  supmul  12230  hashf1lem2  14468  hashf1  14469  mreiincl  17602  efgval  19709  efger  19710  birthdaylem3  26976  disjex  32510  disjexc  32511  mppsval  35411  mblfinlem3  37371  ismblfin  37373  itg2addnc  37386  sdclem1  37455  upbdrech  44954