Theorem abn0 3954

Description: Nonempty class abstraction. See also ab0 3951. (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 2766	. . 3 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
2	1	n0f 3927	. 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑})
3		abid 2610	. . 3 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
4	3	exbii 1774	. 2 ⊢ (∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥𝜑)
5	2, 4	bitri 264	1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Syntax hints:   ↔ wb 196  ∃wex 1704   ∈ wcel 1990  {cab 2608   ≠ wne 2794  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  rabn0OLD  3959  intexab  4822  iinexg  4824  relimasn  5488  inisegn0  5497  mapprc  7861  modom  8161  tz9.1c  8606  scott0  8749  scott0s  8751  cp  8754  karden  8758  acnrcl  8865  aceq3lem  8943  cff  9070  cff1  9080  cfss  9087  domtriomlem  9264  axdclem  9341  nqpr  9836  supadd  10991  supmul  10995  hashf1lem2  13240  hashf1  13241  mreiincl  16256  efgval  18130  efger  18131  birthdaylem3  24680  disjex  29405  disjexc  29406  mppsval  31469  mblfinlem3  33448  ismblfin  33450  itg2addnc  33464  sdclem1  33539  upbdrech  39519