Theorem eqabi 2870

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

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

Syntax hints:   ↔ wb 206   = wceq 1540  ⊤wtru 1541   ∈ wcel 2108  {cab 2713

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809

This theorem is referenced by:  abid1  2871  cbvralcsf  3916  cbvreucsf  3918  cbvrabcsf  3919  dfsymdif4  4234  dfsymdif2  4236  dfpr2  4622  dftp2  4667  iunid  5036  0iin  5040  pwpwab  5079  epse  5636  pwvabrel  5705  fv3  6894  fo1st  8008  fo2nd  8009  xp2  8025  tfrlem3  8392  ixpconstg  8920  ixp0x  8940  ruv  9616  dfom4  9663  cardnum  10108  alephiso  10112  nnzrab  12620  nn0zrab  12621  qnnen  16231  bdayfo  27641  madeval2  27813  h2hcau  30960  dfch2  31388  hhcno  31885  hhcnf  31886  pjhmopidm  32164  fobigcup  35918  dfsingles2  35939  dfrecs2  35968  dfrdg4  35969  dfint3  35970  bj-snglinv  36990  ecres  38296  dfdm6  38319  ruvALT  42692  rp-abid  43402  dfuniv2  44326  compeq  44464  dfnrm2  48906  dfnrm3  48907  dftermc2  49405  dftermc3  49416