Theorem eqabi 2864

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804

This theorem is referenced by:  abid1  2865  cbvralcsf  3907  cbvreucsf  3909  cbvrabcsf  3910  dfsymdif4  4225  dfsymdif2  4227  dfpr2  4613  dftp2  4658  iunid  5027  0iin  5031  pwpwab  5070  epse  5623  pwvabrel  5692  fv3  6879  fo1st  7991  fo2nd  7992  xp2  8008  tfrlem3  8349  ixpconstg  8882  ixp0x  8902  ruv  9562  dfom4  9609  cardnum  10054  alephiso  10058  nnzrab  12568  nn0zrab  12569  qnnen  16188  bdayfo  27596  madeval2  27768  h2hcau  30915  dfch2  31343  hhcno  31840  hhcnf  31841  pjhmopidm  32119  fobigcup  35895  dfsingles2  35916  dfrecs2  35945  dfrdg4  35946  dfint3  35947  bj-snglinv  36967  ecres  38274  dfdm6  38296  ruvALT  42664  rp-abid  43374  dfuniv2  44298  compeq  44436  dfnrm2  48924  dfnrm3  48925  dftermc2  49513  dftermc3  49524