Theorem eqabi 2898

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

Syntax hints:   ↔ wb 209   = wceq 1570  ⊤wtru 1571   ∈ wcel 2143  {cab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838

This theorem is referenced by:  abid1  2899  cbvralcsf  3896  cbvreucsf  3898  cbvrabcsf  3899  dfsymdif4  4213  dfsymdif2  4215  dfpr2  4611  dftp2  4658  iunid  5026  0iin  5029  pwpwab  5070  epse  5645  pwvabrel  5714  fv3  6901  fo1st  8007  fo2nd  8008  xp2  8024  tfrlem3  8365  ixpconstg  8905  ixp0x  8925  ruv  9571  dfom4  9619  cardnum  10079  alephiso  10083  nnzrab  12623  nn0zrab  12624  qnnen  16270  bdayfo  27822  madeval2  28007  h2hcau  31312  dfch2  31740  hhcno  32237  hhcnf  32238  pjhmopidm  32516  fobigcup  36371  dfsingles2  36392  dfrecs2  36423  dfrdg4  36424  dfint3  36425  bj-snglinv  37589  eqrabi  38886  ecres  38915  dfdm6  38937  ruvALT  43384  rp-abid  44088  dfuniv2  44995  compeq  45132  dfnrm2  49693  dfnrm3  49694  dftermc2  50281  dftermc3  50292