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

Theorem abn0 4152
Description: Nonempty class abstraction. See also ab0 4149. (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 2949 . . 3 𝑥{𝑥𝜑}
21n0f 4126 . 2 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥 𝑥 ∈ {𝑥𝜑})
3 abid 2793 . . 3 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
43exbii 1936 . 2 (∃𝑥 𝑥 ∈ {𝑥𝜑} ↔ ∃𝑥𝜑)
52, 4bitri 266 1 ({𝑥𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wex 1859  wcel 2158  {cab 2791  wne 2977  c0 4113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-v 3392  df-dif 3769  df-nul 4114
This theorem is referenced by:  intexab  5011  iinexg  5013  relimasn  5695  inisegn0  5704  mapprc  8093  modom  8397  tz9.1c  8850  scott0  8993  scott0s  8995  cp  8998  karden  9002  acnrcl  9145  aceq3lem  9223  cff  9352  cff1  9362  cfss  9369  domtriomlem  9546  axdclem  9623  nqpr  10118  supadd  11273  supmul  11277  hashf1lem2  13453  hashf1  13454  mreiincl  16457  efgval  18327  efger  18328  birthdaylem3  24890  disjex  29727  disjexc  29728  mppsval  31789  mblfinlem3  33758  ismblfin  33760  itg2addnc  33773  sdclem1  33847  upbdrech  39997
  Copyright terms: Public domain W3C validator