Theorem abbi2i 2955

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

Syntax hints:   ↔ wb 208   = wceq 1537  ⊤wtru 1538   ∈ wcel 2114  {cab 2801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895

This theorem is referenced by:  abid1  2958  cbvralcsf  3927  cbvreucsf  3929  cbvrabcsf  3930  dfsymdif4  4227  dfsymdif2  4229  dfnul2OLD  4296  dfpr2  4588  dftp2  4629  0iin  4989  pwpwab  5027  epse  5540  pwvabrel  5605  fv3  6690  fo1st  7711  fo2nd  7712  xp2  7728  tfrlem3  8016  ixpconstg  8472  ixp0x  8492  dfom4  9114  cardnum  9522  alephiso  9526  nnzrab  12013  nn0zrab  12014  qnnen  15568  h2hcau  28758  dfch2  29186  hhcno  29683  hhcnf  29684  pjhmopidm  29962  bdayfo  33184  madeval2  33292  fobigcup  33363  dfsingles2  33384  dfrecs2  33413  dfrdg4  33414  dfint3  33415  bj-snglinv  34286  bj-df-nul  34350  ecres  35537  dfdm6  35561  compeq  40779