Theorem eqabi 2899

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ⊤wtru 1571   ∈ wcel 2147  {cab 2741

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839

This theorem is used by:  abid1  2900  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  dfsymdif4  4207  dfsymdif2  4209  dfpr2  4605  dftp2  4652  iunid  5022  0iin  5025  pwpwab  5066  epse  5638  pwvabrel  5707  fv3  6929  fo1st  8048  fo2nd  8049  xp2  8065  tfrlem3  8416  ixpconstg  8965  ixp0x  8985  ruv  9632  dfom4  9680  cardnum  10203  alephiso  10207  nnzrab  12754  nn0zrab  12755  qnnen  16413  bdayfo  28067  madeval2  28252  h2hcau  31614  dfch2  32042  hhcno  32539  hhcnf  32540  pjhmopidm  32818  fobigcup  36853  dfsingles2  36874  dfrecs2  36905  dfrdg4  36906  dfint3  36907  bj-snglinv  38076  eqrabi  39391  ecres  39420  dfdm6  39442  ruvALT  43884  rp-abid  44583  dfuniv2  45489  compeq  45625  dfnrm2  50261  dfnrm3  50262  dftermc2  50870  dftermc3  50881