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

Theorem abn0 3928
Description: Nonempty class abstraction. See also ab0 3925. (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 2763 . . 3 𝑥{𝑥𝜑}
21n0f 3903 . 2 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥 𝑥 ∈ {𝑥𝜑})
3 abid 2609 . . 3 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
43exbii 1771 . 2 (∃𝑥 𝑥 ∈ {𝑥𝜑} ↔ ∃𝑥𝜑)
52, 4bitri 264 1 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wex 1701  wcel 1987  {cab 2607  wne 2790  c0 3891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-v 3188  df-dif 3558  df-nul 3892
This theorem is referenced by:  rabn0OLD  3933  intexab  4782  iinexg  4784  relimasn  5447  inisegn0  5456  mapprc  7806  modom  8105  tz9.1c  8550  scott0  8693  scott0s  8695  cp  8698  karden  8702  acnrcl  8809  aceq3lem  8887  cff  9014  cff1  9024  cfss  9031  domtriomlem  9208  axdclem  9285  nqpr  9780  supadd  10935  supmul  10939  hashf1lem2  13178  hashf1  13179  mreiincl  16177  efgval  18051  efger  18052  birthdaylem3  24580  disjex  29247  disjexc  29248  mppsval  31174  mblfinlem3  33077  ismblfin  33079  itg2addnc  33093  sdclem1  33168  upbdrech  38980
  Copyright terms: Public domain W3C validator