Theorem abn0 4334

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

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		ab0 4329	. . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
2	1	notbii 323	. 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑)
3		df-ne 2956	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅)
4		df-ex 1813	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 306	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1812  {cab 2738   ≠ wne 2955  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-ne 2956  df-dif 3902  df-nul 4280

This theorem is used by:  intexab  5310  iinexg  5312  inisegn0  6094  mapprc  8830  modom  9221  tz9.1c  9709  scott0b  9876  scott0OLD  9877  scott0bs  9883  scott0bsOLD  9884  cp  9893  karden  9898  kardenOLD  9899  acnrcl  10045  aceq3lem  10123  cff  10249  cff1  10260  cfss  10267  domtriomlem  10444  axdclem  10521  nqpr  11023  supadd  12207  supmul  12211  hashf1lem2  14521  hashf1  14522  mreiincl  17680  efgval  19844  efger  19845  birthdaylem3  27190  disjex  33065  disjexc  33066  axregs  35665  kardeq0  35682  mppsval  36151  regsfromunir1  37159  mblfinlem3  38408  ismblfin  38410  itg2addnc  38423  sdclem1  38493  upbdrech  46138