Theorem abbi2i 2871

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

Syntax hints:   ↔ wb 209   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114  {cab 2716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811

This theorem is referenced by:  abid1  2873  cbvralcsf  3832  cbvreucsf  3834  cbvrabcsf  3835  dfsymdif4  4139  dfsymdif2  4141  dfpr2  4535  dftp2  4580  0iin  4949  pwpwab  4988  epse  5508  pwvabrel  5574  fv3  6692  fo1st  7734  fo2nd  7735  xp2  7751  tfrlem3  8043  ixpconstg  8516  ixp0x  8536  ruv  9139  dfom4  9185  cardnum  9594  alephiso  9598  nnzrab  12091  nn0zrab  12092  qnnen  15658  h2hcau  28914  dfch2  29342  hhcno  29839  hhcnf  29840  pjhmopidm  30118  bdayfo  33521  madeval2  33678  fobigcup  33840  dfsingles2  33861  dfrecs2  33890  dfrdg4  33891  dfint3  33892  bj-snglinv  34785  ecres  36036  dfdm6  36060  ruvALT  39759  compeq  41596  dfnrm2  45747  dfnrm3  45748