Theorem eqabi 2865

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2147. (Revised by Wolf Lammen, 6-May-2023.)

Hypothesis

Ref	Expression
eqabi.1	⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Assertion

Ref	Expression
eqabi	⊢ 𝐴 = {𝑥 ∣ 𝜑}

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem eqabi

Step	Hyp	Ref	Expression
1		eqabi.1	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)
2	1	a1i 11	. . 3 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
3	2	eqabdv 2863	. 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
4	3	mptru 1541	1 ⊢ 𝐴 = {𝑥 ∣ 𝜑}

Syntax hints:   ↔ wb 205   = wceq 1534  ⊤wtru 1535   ∈ wcel 2099  {cab 2705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806

This theorem is referenced by:  abid1  2866  cbvralcsf  3937  cbvreucsf  3939  cbvrabcsf  3940  dfsymdif4  4249  dfsymdif2  4251  dfpr2  4648  dftp2  4694  iunid  5063  0iin  5067  pwpwab  5106  epse  5661  pwvabrel  5729  fv3  6915  fo1st  8013  fo2nd  8014  xp2  8030  tfrlem3  8398  ixpconstg  8924  ixp0x  8944  ruv  9625  dfom4  9672  cardnum  10117  alephiso  10121  nnzrab  12620  nn0zrab  12621  qnnen  16189  bdayfo  27609  madeval2  27779  h2hcau  30788  dfch2  31216  hhcno  31713  hhcnf  31714  pjhmopidm  31992  fobigcup  35496  dfsingles2  35517  dfrecs2  35546  dfrdg4  35547  dfint3  35548  bj-snglinv  36451  ecres  37750  dfdm6  37773  ruvALT  42093  rp-abid  42807  dfuniv2  43739  compeq  43877  dfnrm2  47950  dfnrm3  47951