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

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

Proof of Theorem eqabi
StepHypRef Expression
1 eqabi.1 . . . 4 (𝑥𝐴𝜑)
21a1i 11 . . 3 (⊤ → (𝑥𝐴𝜑))
32eqabdv 2868 . 2 (⊤ → 𝐴 = {𝑥𝜑})
43mptru 1549 1 𝐴 = {𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wtru 1543  wcel 2107  {cab 2710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811
This theorem is referenced by:  abid1  2871  cbvralcsf  3936  cbvreucsf  3938  cbvrabcsf  3939  dfsymdif4  4246  dfsymdif2  4248  dfpr2  4643  dftp2  4689  iunid  5059  0iin  5063  pwpwab  5102  epse  5655  pwvabrel  5722  fv3  6899  fo1st  7982  fo2nd  7983  xp2  7999  tfrlem3  8365  ixpconstg  8888  ixp0x  8908  ruv  9584  dfom4  9631  cardnum  10076  alephiso  10080  nnzrab  12577  nn0zrab  12578  qnnen  16143  bdayfo  27147  madeval2  27315  h2hcau  30197  dfch2  30625  hhcno  31122  hhcnf  31123  pjhmopidm  31401  fobigcup  34803  dfsingles2  34824  dfrecs2  34853  dfrdg4  34854  dfint3  34855  bj-snglinv  35758  ecres  37052  dfdm6  37076  ruvALT  40934  rp-abid  41999  dfuniv2  42932  compeq  43070  dfnrm2  47404  dfnrm3  47405
  Copyright terms: Public domain W3C validator