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

Theorem abbi2i 2871
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2162. (Revised by Wolf Lammen, 6-May-2023.)
Hypothesis
Ref Expression
abbi2i.1 (𝑥𝐴𝜑)
Assertion
Ref Expression
abbi2i 𝐴 = {𝑥𝜑}
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem abbi2i
StepHypRef Expression
1 abbi2i.1 . . . 4 (𝑥𝐴𝜑)
21a1i 11 . . 3 (⊤ → (𝑥𝐴𝜑))
32abbi2dv 2869 . 2 (⊤ → 𝐴 = {𝑥𝜑})
43mptru 1549 1 𝐴 = {𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1542  wtru 1543  wcel 2114  {cab 2716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811
This theorem is referenced by:  abid1  2873  cbvralcsf  3832  cbvreucsf  3834  cbvrabcsf  3835  dfsymdif4  4139  dfsymdif2  4141  dfpr2  4535  dftp2  4580  0iin  4949  pwpwab  4988  epse  5508  pwvabrel  5574  fv3  6692  fo1st  7734  fo2nd  7735  xp2  7751  tfrlem3  8043  ixpconstg  8516  ixp0x  8536  ruv  9139  dfom4  9185  cardnum  9594  alephiso  9598  nnzrab  12091  nn0zrab  12092  qnnen  15658  h2hcau  28914  dfch2  29342  hhcno  29839  hhcnf  29840  pjhmopidm  30118  bdayfo  33521  madeval2  33678  fobigcup  33840  dfsingles2  33861  dfrecs2  33890  dfrdg4  33891  dfint3  33892  bj-snglinv  34785  ecres  36036  dfdm6  36060  ruvALT  39759  compeq  41596  dfnrm2  45747  dfnrm3  45748
  Copyright terms: Public domain W3C validator