Theorem abbi2i 2953

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 2950	. 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
4	3	mptru 1544	1 ⊢ 𝐴 = {𝑥 ∣ 𝜑}

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

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 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893

This theorem is referenced by:  abid1  2956  cbvralcsf  3925  cbvreucsf  3927  cbvrabcsf  3928  dfsymdif4  4225  dfsymdif2  4227  dfnul2OLD  4294  dfpr2  4586  dftp2  4627  0iin  4987  pwpwab  5025  epse  5538  pwvabrel  5603  fv3  6688  fo1st  7709  fo2nd  7710  xp2  7726  tfrlem3  8014  ixpconstg  8470  ixp0x  8490  dfom4  9112  cardnum  9520  alephiso  9524  nnzrab  12011  nn0zrab  12012  qnnen  15566  h2hcau  28756  dfch2  29184  hhcno  29681  hhcnf  29682  pjhmopidm  29960  bdayfo  33182  madeval2  33290  fobigcup  33361  dfsingles2  33382  dfrecs2  33411  dfrdg4  33412  dfint3  33413  bj-snglinv  34287  bj-df-nul  34351  ecres  35550  dfdm6  35574  compeq  40792