Theorem eqabi 2876

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

Syntax hints:   ↔ wb 208   = wceq 1548  ⊤wtru 1549   ∈ wcel 2121  {cab 2719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816

This theorem is referenced by:  abid1  2877  cbvralcsf  3874  cbvreucsf  3876  cbvrabcsf  3877  dfsymdif4  4189  dfsymdif2  4191  dfpr2  4578  dftp2  4625  iunid  4992  0iin  4995  pwpwab  5034  epse  5602  pwvabrel  5671  fv3  6848  fo1st  7953  fo2nd  7954  xp2  7970  tfrlem3  8310  ixpconstg  8848  ixp0x  8868  ruv  9517  dfom4  9565  cardnum  10011  alephiso  10015  nnzrab  12550  nn0zrab  12551  qnnen  16175  bdayfo  27661  madeval2  27845  h2hcau  31070  dfch2  31498  hhcno  31995  hhcnf  31996  pjhmopidm  32274  fobigcup  36139  dfsingles2  36160  dfrecs2  36191  dfrdg4  36192  dfint3  36193  bj-snglinv  37338  eqrabi  38636  ecres  38665  dfdm6  38687  ruvALT  43132  rp-abid  43836  dfuniv2  44759  compeq  44896  dfnrm2  49434  dfnrm3  49435  dftermc2  50022  dftermc3  50033