Theorem eqabi 2900

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2194. (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

Step	Hyp	Ref	Expression
1		eqabi.1	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)
2	1	a1i 11	. . 3 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
3	2	eqabdv 2898	. 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
4	3	mptru 1570	1 ⊢ 𝐴 = {𝑥 ∣ 𝜑}

Syntax hints:   ↔ wb 209   = wceq 1563  ⊤wtru 1564   ∈ wcel 2145  {cab 2743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840

This theorem is referenced by:  abid1  2901  cbvralcsf  3897  cbvreucsf  3899  cbvrabcsf  3900  dfsymdif4  4214  dfsymdif2  4216  dfpr2  4606  dftp2  4653  iunid  5020  0iin  5023  pwpwab  5064  epse  5633  pwvabrel  5702  fv3  6889  fo1st  7994  fo2nd  7995  xp2  8011  tfrlem3  8352  ixpconstg  8892  ixp0x  8912  ruv  9558  dfom4  9606  cardnum  10066  alephiso  10070  nnzrab  12610  nn0zrab  12611  qnnen  16257  bdayfo  27795  madeval2  27980  h2hcau  31236  dfch2  31664  hhcno  32161  hhcnf  32162  pjhmopidm  32440  fobigcup  36256  dfsingles2  36277  dfrecs2  36308  dfrdg4  36309  dfint3  36310  bj-snglinv  37464  eqrabi  38762  ecres  38791  dfdm6  38813  ruvALT  43258  rp-abid  43962  dfuniv2  44871  compeq  45008  dfnrm2  49562  dfnrm3  49563  dftermc2  50150  dftermc3  50161