Theorem abn0 4262

Description: Nonempty class abstraction. See also ab0 4259. (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 2953	. . 3 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
2	1	n0f 4233	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑})
3		abid 2781	. . 3 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
4	3	exbii 1833	. 2 ⊢ (∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥𝜑)
5	2, 4	bitri 276	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Syntax hints:   ↔ wb 207  ∃wex 1765   ∈ wcel 2083  {cab 2777   ≠ wne 2986  ∅c0 4217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-dif 3868  df-nul 4218

This theorem is referenced by:  intexab  5140  iinexg  5142  relimasn  5835  inisegn0  5844  mapprc  8267  modom  8572  tz9.1c  9025  scott0  9168  scott0s  9170  cp  9173  karden  9177  acnrcl  9321  aceq3lem  9399  cff  9523  cff1  9533  cfss  9540  domtriomlem  9717  axdclem  9794  nqpr  10289  supadd  11463  supmul  11467  hashf1lem2  13666  hashf1  13667  mreiincl  16700  efgval  18574  efger  18575  birthdaylem3  25217  disjex  30028  disjexc  30029  mppsval  32429  mblfinlem3  34483  ismblfin  34485  itg2addnc  34498  sdclem1  34571  upbdrech  41134