Theorem eqabi 2897

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145  {cab 2740

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used by:  abid1  2898  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  dfsymdif4  4208  dfsymdif2  4210  dfpr2  4608  dftp2  4655  iunid  5023  0iin  5026  pwpwab  5067  epse  5641  pwvabrel  5710  fv3  6900  fo1st  8010  fo2nd  8011  xp2  8027  tfrlem3  8370  ixpconstg  8917  ixp0x  8937  ruv  9584  dfom4  9632  cardnum  10101  alephiso  10105  nnzrab  12650  nn0zrab  12651  qnnen  16307  bdayfo  27921  madeval2  28106  h2hcau  31468  dfch2  31896  hhcno  32393  hhcnf  32394  pjhmopidm  32672  fobigcup  36485  dfsingles2  36506  dfrecs2  36537  dfrdg4  36538  dfint3  36539  bj-snglinv  37724  eqrabi  39012  ecres  39041  dfdm6  39063  ruvALT  43523  rp-abid  44227  dfuniv2  45134  compeq  45271  dfnrm2  49866  dfnrm3  49867  dftermc2  50454  dftermc3  50465