Theorem eqabi 2875

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

Syntax hints:   ↔ wb 207   = wceq 1547  ⊤wtru 1548   ∈ wcel 2119  {cab 2718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815

This theorem is referenced by:  abid1  2876  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  dfsymdif4  4194  dfsymdif2  4196  dfpr2  4583  dftp2  4630  iunid  4997  0iin  5000  pwpwab  5039  epse  5607  pwvabrel  5676  fv3  6852  fo1st  7958  fo2nd  7959  xp2  7975  tfrlem3  8314  ixpconstg  8851  ixp0x  8871  ruv  9520  dfom4  9568  cardnum  10014  alephiso  10018  nnzrab  12553  nn0zrab  12554  qnnen  16178  bdayfo  27666  madeval2  27850  h2hcau  31075  dfch2  31503  hhcno  32000  hhcnf  32001  pjhmopidm  32279  fobigcup  36133  dfsingles2  36154  dfrecs2  36185  dfrdg4  36186  dfint3  36187  bj-snglinv  37332  eqrabi  38630  ecres  38659  dfdm6  38681  ruvALT  43126  rp-abid  43830  dfuniv2  44753  compeq  44890  dfnrm2  49429  dfnrm3  49430  dftermc2  50017  dftermc3  50028