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

Theorem eqabi 2875
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 2873 . 2 (⊤ → 𝐴 = {𝑥𝜑})
43mptru 1544 1 𝐴 = {𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1537  wtru 1538  wcel 2106  {cab 2712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814
This theorem is referenced by:  abid1  2876  cbvralcsf  3953  cbvreucsf  3955  cbvrabcsf  3956  dfsymdif4  4265  dfsymdif2  4267  dfpr2  4651  dftp2  4696  iunid  5065  0iin  5069  pwpwab  5108  epse  5671  pwvabrel  5740  fv3  6925  fo1st  8033  fo2nd  8034  xp2  8050  tfrlem3  8417  ixpconstg  8945  ixp0x  8965  ruv  9640  dfom4  9687  cardnum  10132  alephiso  10136  nnzrab  12643  nn0zrab  12644  qnnen  16246  bdayfo  27737  madeval2  27907  h2hcau  31008  dfch2  31436  hhcno  31933  hhcnf  31934  pjhmopidm  32212  fobigcup  35882  dfsingles2  35903  dfrecs2  35932  dfrdg4  35933  dfint3  35934  bj-snglinv  36955  ecres  38260  dfdm6  38283  ruvALT  42656  rp-abid  43368  dfuniv2  44298  compeq  44436  dfnrm2  48728  dfnrm3  48729
  Copyright terms: Public domain W3C validator