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

Theorem abbi2i 2956
 Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2160. (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 2953 . 2 (⊤ → 𝐴 = {𝑥𝜑})
43mptru 1543 1 𝐴 = {𝑥𝜑}
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   = wceq 1536  ⊤wtru 1537   ∈ wcel 2113  {cab 2802 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796 This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1539  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896 This theorem is referenced by:  abid1  2959  cbvralcsf  3928  cbvreucsf  3930  cbvrabcsf  3931  dfsymdif4  4228  dfsymdif2  4230  dfnul2OLD  4297  dfpr2  4589  dftp2  4630  0iin  4990  pwpwab  5028  epse  5541  pwvabrel  5606  fv3  6691  fo1st  7712  fo2nd  7713  xp2  7729  tfrlem3  8017  ixpconstg  8473  ixp0x  8493  dfom4  9115  cardnum  9523  alephiso  9527  nnzrab  12013  nn0zrab  12014  qnnen  15569  h2hcau  28759  dfch2  29187  hhcno  29684  hhcnf  29685  pjhmopidm  29963  bdayfo  33186  madeval2  33294  fobigcup  33365  dfsingles2  33386  dfrecs2  33415  dfrdg4  33416  dfint3  33417  bj-snglinv  34288  bj-df-nul  34352  ecres  35539  dfdm6  35563  compeq  40778
 Copyright terms: Public domain W3C validator