Theorem abbi2i 2880

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
abbi2i.1	⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Assertion

Ref	Expression
abbi2i	⊢ 𝐴 = {𝑥 ∣ 𝜑}

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem abbi2i

Step	Hyp	Ref	Expression
1		abbi2i.1	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)
2	1	a1i 11	. . 3 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
3	2	abbi2dv 2878	. 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
4	3	mptru 1546	1 ⊢ 𝐴 = {𝑥 ∣ 𝜑}

Syntax hints:   ↔ wb 205   = wceq 1539  ⊤wtru 1540   ∈ wcel 2107  {cab 2716

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817

This theorem is referenced by:  abid1  2882  cbvralcsf  3878  cbvreucsf  3880  cbvrabcsf  3881  dfsymdif4  4183  dfsymdif2  4185  dfpr2  4581  dftp2  4626  0iin  4994  pwpwab  5033  epse  5573  pwvabrel  5639  fv3  6801  fo1st  7860  fo2nd  7861  xp2  7877  tfrlem3  8218  ixpconstg  8703  ixp0x  8723  ruv  9370  dfom4  9416  cardnum  9859  alephiso  9863  nnzrab  12357  nn0zrab  12358  qnnen  15931  h2hcau  29350  dfch2  29778  hhcno  30275  hhcnf  30276  pjhmopidm  30554  bdayfo  33889  madeval2  34046  fobigcup  34211  dfsingles2  34232  dfrecs2  34261  dfrdg4  34262  dfint3  34263  bj-snglinv  35171  ecres  36421  dfdm6  36444  ruvALT  40175  dfuniv2  41927  compeq  42065  dfnrm2  46236  dfnrm3  46237