Theorem eqabi 2861

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

Syntax hints:   ↔ wb 205   = wceq 1533  ⊤wtru 1534   ∈ wcel 2098  {cab 2701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802

This theorem is referenced by:  abid1  2862  cbvralcsf  3931  cbvreucsf  3933  cbvrabcsf  3934  dfsymdif4  4241  dfsymdif2  4243  dfpr2  4640  dftp2  4686  iunid  5054  0iin  5058  pwpwab  5097  epse  5650  pwvabrel  5718  fv3  6900  fo1st  7989  fo2nd  7990  xp2  8006  tfrlem3  8374  ixpconstg  8897  ixp0x  8917  ruv  9594  dfom4  9641  cardnum  10086  alephiso  10090  nnzrab  12589  nn0zrab  12590  qnnen  16159  bdayfo  27550  madeval2  27720  h2hcau  30726  dfch2  31154  hhcno  31651  hhcnf  31652  pjhmopidm  31930  fobigcup  35394  dfsingles2  35415  dfrecs2  35444  dfrdg4  35445  dfint3  35446  bj-snglinv  36353  ecres  37649  dfdm6  37673  ruvALT  41961  rp-abid  42677  dfuniv2  43610  compeq  43748  dfnrm2  47811  dfnrm3  47812