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

Theorem abeq2i 2925
 Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) (Proof shortened by Wolf Lammen, 15-Nov-2019.)
Hypothesis
Ref Expression
abeq2i.1 𝐴 = {𝑥𝜑}
Assertion
Ref Expression
abeq2i (𝑥𝐴𝜑)

Proof of Theorem abeq2i
StepHypRef Expression
1 abeq2i.1 . . . 4 𝐴 = {𝑥𝜑}
21a1i 11 . . 3 (⊤ → 𝐴 = {𝑥𝜑})
32abeq2d 2924 . 2 (⊤ → (𝑥𝐴𝜑))
43mptru 1545 1 (𝑥𝐴𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1538  ⊤wtru 1539   ∈ wcel 2111  {cab 2776 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870 This theorem is referenced by:  abeq1i  2926  rabid  3331  vexOLD  3445  csbcow  3843  csbco  3844  csbgfi  3848  csbnestgfw  4327  csbnestgf  4332  ssrel  5622  relopabi  5659  cnv0  5967  funcnv3  6395  opabiota  6722  zfrep6  7641  wfrlem2  7941  wfrlem3  7942  wfrlem4  7944  wfrdmcl  7949  tfrlem4  8001  tfrlem8  8006  tfrlem9  8007  ixpn0  8480  sbthlem1  8614  dffi3  8882  1idpr  10443  ltexprlem1  10450  ltexprlem2  10451  ltexprlem3  10452  ltexprlem4  10453  ltexprlem6  10455  ltexprlem7  10456  reclem2pr  10462  reclem3pr  10463  reclem4pr  10464  supsrlem  10525  dissnref  22143  dissnlocfin  22144  txbas  22182  xkoccn  22234  xkoptsub  22269  xkoco1cn  22272  xkoco2cn  22273  xkoinjcn  22302  mbfi1fseqlem4  24332  avril1  28258  rnmposs  30447  bnj1436  32236  bnj916  32330  bnj983  32348  bnj1083  32375  bnj1245  32411  bnj1311  32421  bnj1371  32426  bnj1398  32431  setinds  33151  frrlem2  33252  frrlem3  33253  frrlem4  33254  frrlem8  33258  bj-elsngl  34423  bj-projun  34449  bj-projval  34451  f1omptsnlem  34772  icoreresf  34788  finxp0  34827  finxp1o  34828  finxpsuclem  34833  sdclem1  35200  csbcom2fi  35585
 Copyright terms: Public domain W3C validator