Theorem eqabi 2870

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

Syntax hints:   ↔ wb 205   = wceq 1542  ⊤wtru 1543   ∈ wcel 2107  {cab 2710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811

This theorem is referenced by:  abid1  2871  cbvralcsf  3936  cbvreucsf  3938  cbvrabcsf  3939  dfsymdif4  4246  dfsymdif2  4248  dfpr2  4643  dftp2  4689  iunid  5059  0iin  5063  pwpwab  5102  epse  5655  pwvabrel  5722  fv3  6899  fo1st  7982  fo2nd  7983  xp2  7999  tfrlem3  8365  ixpconstg  8888  ixp0x  8908  ruv  9584  dfom4  9631  cardnum  10076  alephiso  10080  nnzrab  12577  nn0zrab  12578  qnnen  16143  bdayfo  27147  madeval2  27315  h2hcau  30197  dfch2  30625  hhcno  31122  hhcnf  31123  pjhmopidm  31401  fobigcup  34803  dfsingles2  34824  dfrecs2  34853  dfrdg4  34854  dfint3  34855  bj-snglinv  35758  ecres  37052  dfdm6  37076  ruvALT  40934  rp-abid  41999  dfuniv2  42932  compeq  43070  dfnrm2  47404  dfnrm3  47405