Theorem eqabi 2895

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ⊤wtru 1570   ∈ wcel 2144  {cab 2738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  abid1  2896  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  dfsymdif4  4204  dfsymdif2  4206  dfpr2  4601  dftp2  4648  iunid  5018  0iin  5021  pwpwab  5062  epse  5632  pwvabrel  5701  fv3  6904  fo1st  8022  fo2nd  8023  xp2  8039  tfrlem3  8389  ixpconstg  8938  ixp0x  8958  ruv  9606  dfom4  9654  cardnum  10177  alephiso  10181  nnzrab  12728  nn0zrab  12729  qnnen  16387  bdayfo  28040  madeval2  28225  h2hcau  31587  dfch2  32015  hhcno  32512  hhcnf  32513  pjhmopidm  32791  fobigcup  36755  dfsingles2  36776  dfrecs2  36807  dfrdg4  36808  dfint3  36809  bj-snglinv  37978  eqrabi  39282  ecres  39311  dfdm6  39333  ruvALT  43774  rp-abid  44474  dfuniv2  45380  compeq  45517  dfnrm2  50140  dfnrm3  50141  dftermc2  50749  dftermc3  50760