Theorem abn0 4152

Description: Nonempty class abstraction. See also ab0 4149. (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 2949	. . 3 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
2	1	n0f 4126	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑})
3		abid 2793	. . 3 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
4	3	exbii 1936	. 2 ⊢ (∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥𝜑)
5	2, 4	bitri 266	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Syntax hints:   ↔ wb 197  ∃wex 1859   ∈ wcel 2158  {cab 2791   ≠ wne 2977  ∅c0 4113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-v 3392  df-dif 3769  df-nul 4114

This theorem is referenced by:  intexab  5011  iinexg  5013  relimasn  5695  inisegn0  5704  mapprc  8093  modom  8397  tz9.1c  8850  scott0  8993  scott0s  8995  cp  8998  karden  9002  acnrcl  9145  aceq3lem  9223  cff  9352  cff1  9362  cfss  9369  domtriomlem  9546  axdclem  9623  nqpr  10118  supadd  11273  supmul  11277  hashf1lem2  13453  hashf1  13454  mreiincl  16457  efgval  18327  efger  18328  birthdaylem3  24890  disjex  29727  disjexc  29728  mppsval  31789  mblfinlem3  33758  ismblfin  33760  itg2addnc  33773  sdclem1  33847  upbdrech  39997