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

Theorem eqabi 2861
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2146. (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 2859 . 2 (⊤ → 𝐴 = {𝑥𝜑})
43mptru 1540 1 𝐴 = {𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1533  wtru 1534  wcel 2098  {cab 2702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802
This theorem is referenced by:  abid1  2862  cbvralcsf  3934  cbvreucsf  3936  cbvrabcsf  3937  dfsymdif4  4247  dfsymdif2  4249  dfpr2  4650  dftp2  4695  iunid  5064  0iin  5068  pwpwab  5107  epse  5661  pwvabrel  5729  fv3  6914  fo1st  8014  fo2nd  8015  xp2  8031  tfrlem3  8399  ixpconstg  8925  ixp0x  8945  ruv  9627  dfom4  9674  cardnum  10119  alephiso  10123  nnzrab  12623  nn0zrab  12624  qnnen  16193  bdayfo  27656  madeval2  27826  h2hcau  30861  dfch2  31289  hhcno  31786  hhcnf  31787  pjhmopidm  32065  fobigcup  35627  dfsingles2  35648  dfrecs2  35677  dfrdg4  35678  dfint3  35679  bj-snglinv  36582  ecres  37880  dfdm6  37903  ruvALT  42228  rp-abid  42949  dfuniv2  43881  compeq  44019  dfnrm2  48136  dfnrm3  48137
  Copyright terms: Public domain W3C validator
OSZAR »