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

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
StepHypRef Expression
1 nfab1 2953 . . 3 𝑥{𝑥𝜑}
21n0f 4233 . 2 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥 𝑥 ∈ {𝑥𝜑})
3 abid 2781 . . 3 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
43exbii 1833 . 2 (∃𝑥 𝑥 ∈ {𝑥𝜑} ↔ ∃𝑥𝜑)
52, 4bitri 276 1 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator