Theorem abbi2i 2929

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

Syntax hints:   ↔ wb 209   = wceq 1538  ⊤wtru 1539   ∈ wcel 2111  {cab 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870

This theorem is referenced by:  abid1  2931  cbvralcsf  3870  cbvreucsf  3872  cbvrabcsf  3873  dfsymdif4  4175  dfsymdif2  4177  dfpr2  4544  dftp2  4587  0iin  4950  pwpwab  4988  epse  5502  pwvabrel  5567  fv3  6663  fo1st  7691  fo2nd  7692  xp2  7708  tfrlem3  7997  ixpconstg  8453  ixp0x  8473  dfom4  9096  cardnum  9505  alephiso  9509  nnzrab  11998  nn0zrab  11999  qnnen  15558  h2hcau  28762  dfch2  29190  hhcno  29687  hhcnf  29688  pjhmopidm  29966  bdayfo  33295  madeval2  33403  fobigcup  33474  dfsingles2  33495  dfrecs2  33524  dfrdg4  33525  dfint3  33526  bj-snglinv  34408  bj-df-nul  34472  ecres  35695  dfdm6  35719  compeq  41144