Theorem eqabi 2901

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ⊤wtru 1571   ∈ wcel 2146  {cab 2744

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841

This theorem is used by:  abid1  2902  cbvralcsf  3898  cbvreucsf  3900  cbvrabcsf  3901  dfsymdif4  4215  dfsymdif2  4217  dfpr2  4615  dftp2  4662  iunid  5030  0iin  5033  pwpwab  5074  epse  5648  pwvabrel  5717  fv3  6906  fo1st  8015  fo2nd  8016  xp2  8032  tfrlem3  8373  ixpconstg  8913  ixp0x  8933  ruv  9580  dfom4  9628  cardnum  10097  alephiso  10101  nnzrab  12640  nn0zrab  12641  qnnen  16294  bdayfo  27878  madeval2  28063  h2hcau  31368  dfch2  31796  hhcno  32293  hhcnf  32294  pjhmopidm  32572  fobigcup  36411  dfsingles2  36432  dfrecs2  36463  dfrdg4  36464  dfint3  36465  bj-snglinv  37649  eqrabi  38946  ecres  38975  dfdm6  38997  ruvALT  43442  rp-abid  44146  dfuniv2  45053  compeq  45190  dfnrm2  49751  dfnrm3  49752  dftermc2  50339  dftermc3  50350