MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abn0 Structured version   Visualization version   GIF version

Theorem abn0 3987
Description: Nonempty class abstraction. See also ab0 3984. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
Assertion
Ref Expression
abn0 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥𝜑)

Proof of Theorem abn0
StepHypRef Expression
1 nfab1 2795 . . 3 𝑥{𝑥𝜑}
21n0f 3960 . 2 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥 𝑥 ∈ {𝑥𝜑})
3 abid 2639 . . 3 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
43exbii 1814 . 2 (∃𝑥 𝑥 ∈ {𝑥𝜑} ↔ ∃𝑥𝜑)
52, 4bitri 264 1 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wex 1744  wcel 2030  {cab 2637  wne 2823  c0 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-v 3233  df-dif 3610  df-nul 3949
This theorem is referenced by:  rabn0OLD  3992  intexab  4852  iinexg  4854  relimasn  5523  inisegn0  5532  mapprc  7903  modom  8202  tz9.1c  8644  scott0  8787  scott0s  8789  cp  8792  karden  8796  acnrcl  8903  aceq3lem  8981  cff  9108  cff1  9118  cfss  9125  domtriomlem  9302  axdclem  9379  nqpr  9874  supadd  11029  supmul  11033  hashf1lem2  13278  hashf1  13279  mreiincl  16303  efgval  18176  efger  18177  birthdaylem3  24725  disjex  29531  disjexc  29532  mppsval  31595  mblfinlem3  33578  ismblfin  33580  itg2addnc  33594  sdclem1  33669  upbdrech  39833
  Copyright terms: Public domain W3C validator