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

Theorem abbi2i 2881
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
abbi2i.1 (𝑥𝐴𝜑)
Assertion
Ref Expression
abbi2i 𝐴 = {𝑥𝜑}
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem abbi2i
StepHypRef Expression
1 abeq2 2875 . 2 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
2 abbi2i.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1894 1 𝐴 = {𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1652  wcel 2155  {cab 2751
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761
This theorem is referenced by:  abid1  2887  cbvralcsf  3725  cbvreucsf  3727  cbvrabcsf  3728  dfsymdif4  4013  dfsymdif2  4015  symdif2OLD  4020  dfnul2  4083  dfpr2  4355  dftp2  4389  0iin  4736  pwpwab  4773  epse  5262  fv3  6395  fo1st  7388  fo2nd  7389  xp2  7405  tfrlem3  7680  ixpconstg  8124  ixp0x  8143  dfom4  8763  cardnum  9170  alephiso  9174  nnzrab  11655  nn0zrab  11656  qnnen  15227  h2hcau  28295  dfch2  28725  hhcno  29222  hhcnf  29223  pjhmopidm  29501  bdayfo  32275  madeval2  32383  fobigcup  32454  dfsingles2  32475  dfrecs2  32504  dfrdg4  32505  dfint3  32506  bj-snglinv  33390  ecres  34478  dfdm6  34505  compeq  39318
  Copyright terms: Public domain W3C validator