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

Theorem abbi2i 2874
Description: Equality of a class variable and a class abstraction (inference rule). (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 2868 . 2 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
2 abbi2i.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1873 1 𝐴 = {𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1630  wcel 2137  {cab 2744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754
This theorem is referenced by:  abid1  2880  cbvralcsf  3704  cbvreucsf  3706  cbvrabcsf  3707  dfsymdif2  3992  symdif2  3993  dfnul2  4058  dfpr2  4337  dftp2  4373  0iin  4728  pwpwab  4764  epse  5247  fv3  6365  fo1st  7351  fo2nd  7352  xp2  7368  tfrlem3  7641  mapsn  8063  ixpconstg  8081  ixp0x  8100  dfom4  8717  cardnum  9105  alephiso  9109  nnzrab  11595  nn0zrab  11596  qnnen  15139  h2hcau  28143  dfch2  28573  hhcno  29070  hhcnf  29071  pjhmopidm  29349  bdayfo  32132  madeval2  32240  fobigcup  32311  dfsingles2  32332  dfrecs2  32361  dfrdg4  32362  dfint3  32363  bj-snglinv  33264  ecres  34365  dfdm6  34393  compeq  39142
  Copyright terms: Public domain W3C validator