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

Theorem eqabi 2877
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2157. (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 2875 . 2 (⊤ → 𝐴 = {𝑥𝜑})
43mptru 1547 1 𝐴 = {𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  wtru 1541  wcel 2108  {cab 2714
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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816
This theorem is referenced by:  abid1  2878  cbvralcsf  3941  cbvreucsf  3943  cbvrabcsf  3944  dfsymdif4  4259  dfsymdif2  4261  dfpr2  4646  dftp2  4691  iunid  5060  0iin  5064  pwpwab  5103  epse  5667  pwvabrel  5736  fv3  6924  fo1st  8034  fo2nd  8035  xp2  8051  tfrlem3  8418  ixpconstg  8946  ixp0x  8966  ruv  9642  dfom4  9689  cardnum  10134  alephiso  10138  nnzrab  12645  nn0zrab  12646  qnnen  16249  bdayfo  27722  madeval2  27892  h2hcau  30998  dfch2  31426  hhcno  31923  hhcnf  31924  pjhmopidm  32202  fobigcup  35901  dfsingles2  35922  dfrecs2  35951  dfrdg4  35952  dfint3  35953  bj-snglinv  36973  ecres  38279  dfdm6  38302  ruvALT  42679  rp-abid  43391  dfuniv2  44321  compeq  44459  dfnrm2  48829  dfnrm3  48830  dftermc2  49150
  Copyright terms: Public domain W3C validator