Theorem eqabi 2863

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 2861	. 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
4	3	mptru 1547	1 ⊢ 𝐴 = {𝑥 ∣ 𝜑}

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  abid1  2864  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  dfsymdif4  4212  dfsymdif2  4214  dfpr2  4600  dftp2  4645  iunid  5012  0iin  5016  pwpwab  5055  epse  5605  pwvabrel  5674  fv3  6844  fo1st  7951  fo2nd  7952  xp2  7968  tfrlem3  8307  ixpconstg  8840  ixp0x  8860  ruv  9516  dfom4  9564  cardnum  10007  alephiso  10011  nnzrab  12521  nn0zrab  12522  qnnen  16140  bdayfo  27605  madeval2  27781  h2hcau  30941  dfch2  31369  hhcno  31866  hhcnf  31867  pjhmopidm  32145  fobigcup  35876  dfsingles2  35897  dfrecs2  35926  dfrdg4  35927  dfint3  35928  bj-snglinv  36948  ecres  38255  dfdm6  38277  ruvALT  42645  rp-abid  43354  dfuniv2  44278  compeq  44416  dfnrm2  48920  dfnrm3  48921  dftermc2  49509  dftermc3  49520