Theorem abn0 4339

Description: Nonempty class abstraction. See also ab0 4336. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)

Assertion

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

Proof of Theorem abn0

Step	Hyp	Ref	Expression
1		nfab1 2982	. . 3 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
2	1	n0f 4310	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑})
3		abid 2806	. . 3 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
4	3	exbii 1847	. 2 ⊢ (∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥𝜑)
5	2, 4	bitri 277	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Syntax hints:   ↔ wb 208  ∃wex 1779   ∈ wcel 2113  {cab 2802   ≠ wne 3019  ∅c0 4294

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-dif 3942  df-nul 4295

This theorem is referenced by:  intexab  5245  iinexg  5247  relimasn  5955  inisegn0  5964  mapprc  8413  modom  8722  tz9.1c  9175  scott0  9318  scott0s  9320  cp  9323  karden  9327  acnrcl  9471  aceq3lem  9549  cff  9673  cff1  9683  cfss  9690  domtriomlem  9867  axdclem  9944  nqpr  10439  supadd  11612  supmul  11616  hashf1lem2  13817  hashf1  13818  mreiincl  16870  efgval  18846  efger  18847  birthdaylem3  25534  disjex  30345  disjexc  30346  mppsval  32823  mblfinlem3  34935  ismblfin  34937  itg2addnc  34950  sdclem1  35022  upbdrech  41578