Theorem abbi2i 2878

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817

This theorem is referenced by:  abid1  2880  cbvralcsf  3873  cbvreucsf  3875  cbvrabcsf  3876  dfsymdif4  4179  dfsymdif2  4181  dfpr2  4577  dftp2  4622  0iin  4989  pwpwab  5028  epse  5563  pwvabrel  5629  fv3  6774  fo1st  7824  fo2nd  7825  xp2  7841  tfrlem3  8180  ixpconstg  8652  ixp0x  8672  ruv  9291  dfom4  9337  cardnum  9781  alephiso  9785  nnzrab  12278  nn0zrab  12279  qnnen  15850  h2hcau  29242  dfch2  29670  hhcno  30167  hhcnf  30168  pjhmopidm  30446  bdayfo  33807  madeval2  33964  fobigcup  34129  dfsingles2  34150  dfrecs2  34179  dfrdg4  34180  dfint3  34181  bj-snglinv  35089  ecres  36340  dfdm6  36364  ruvALT  40096  dfuniv2  41809  compeq  41947  dfnrm2  46113  dfnrm3  46114