Theorem eqabi 2896

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

Syntax hints:   ↔ wb 208   = wceq 1559  ⊤wtru 1560   ∈ wcel 2141  {cab 2739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is referenced by:  abid1  2897  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  dfsymdif4  4209  dfsymdif2  4211  dfpr2  4600  dftp2  4647  iunid  5015  0iin  5018  pwpwab  5057  epse  5625  pwvabrel  5694  fv3  6879  fo1st  7984  fo2nd  7985  xp2  8001  tfrlem3  8341  ixpconstg  8881  ixp0x  8901  ruv  9549  dfom4  9597  cardnum  10043  alephiso  10047  nnzrab  12592  nn0zrab  12593  qnnen  16235  bdayfo  27728  madeval2  27913  h2hcau  31138  dfch2  31566  hhcno  32063  hhcnf  32064  pjhmopidm  32342  fobigcup  36208  dfsingles2  36229  dfrecs2  36260  dfrdg4  36261  dfint3  36262  bj-snglinv  37417  eqrabi  38715  ecres  38744  dfdm6  38766  ruvALT  43211  rp-abid  43915  dfuniv2  44838  compeq  44975  dfnrm2  49513  dfnrm3  49514  dftermc2  50101  dftermc3  50112