Theorem eqabi 2866

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

Syntax hints:   ↔ wb 206   = wceq 1541  ⊤wtru 1542   ∈ wcel 2111  {cab 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806

This theorem is referenced by:  abid1  2867  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  dfsymdif4  4209  dfsymdif2  4211  dfpr2  4597  dftp2  4644  iunid  5009  0iin  5012  pwpwab  5051  epse  5598  pwvabrel  5667  fv3  6840  fo1st  7941  fo2nd  7942  xp2  7958  tfrlem3  8297  ixpconstg  8830  ixp0x  8850  ruv  9491  dfom4  9539  cardnum  9985  alephiso  9989  nnzrab  12500  nn0zrab  12501  qnnen  16122  bdayfo  27617  madeval2  27795  h2hcau  30957  dfch2  31385  hhcno  31882  hhcnf  31883  pjhmopidm  32161  fobigcup  35940  dfsingles2  35961  dfrecs2  35990  dfrdg4  35991  dfint3  35992  bj-snglinv  37012  ecres  38319  dfdm6  38341  ruvALT  42708  rp-abid  43417  dfuniv2  44341  compeq  44478  dfnrm2  48969  dfnrm3  48970  dftermc2  49558  dftermc3  49569