Theorem eqabi 2880

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2158. (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 2878	. 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
4	3	mptru 1544	1 ⊢ 𝐴 = {𝑥 ∣ 𝜑}

Syntax hints:   ↔ wb 206   = wceq 1537  ⊤wtru 1538   ∈ wcel 2108  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819

This theorem is referenced by:  abid1  2881  cbvralcsf  3966  cbvreucsf  3968  cbvrabcsf  3969  dfsymdif4  4278  dfsymdif2  4280  dfpr2  4668  dftp2  4714  iunid  5083  0iin  5087  pwpwab  5126  epse  5682  pwvabrel  5751  fv3  6938  fo1st  8050  fo2nd  8051  xp2  8067  tfrlem3  8434  ixpconstg  8964  ixp0x  8984  ruv  9671  dfom4  9718  cardnum  10163  alephiso  10167  nnzrab  12671  nn0zrab  12672  qnnen  16261  bdayfo  27740  madeval2  27910  h2hcau  31011  dfch2  31439  hhcno  31936  hhcnf  31937  pjhmopidm  32215  fobigcup  35864  dfsingles2  35885  dfrecs2  35914  dfrdg4  35915  dfint3  35916  bj-snglinv  36938  ecres  38234  dfdm6  38257  ruvALT  42624  rp-abid  43340  dfuniv2  44271  compeq  44409  dfnrm2  48611  dfnrm3  48612