Theorem eqabi 2872

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  abid1  2873  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  dfsymdif4  4213  dfsymdif2  4215  dfpr2  4603  dftp2  4650  iunid  5018  0iin  5021  pwpwab  5060  epse  5614  pwvabrel  5683  fv3  6860  fo1st  7963  fo2nd  7964  xp2  7980  tfrlem3  8319  ixpconstg  8856  ixp0x  8876  ruv  9522  dfom4  9570  cardnum  10016  alephiso  10020  nnzrab  12531  nn0zrab  12532  qnnen  16150  bdayfo  27657  madeval2  27841  h2hcau  31066  dfch2  31494  hhcno  31991  hhcnf  31992  pjhmopidm  32270  fobigcup  36111  dfsingles2  36132  dfrecs2  36163  dfrdg4  36164  dfint3  36165  bj-snglinv  37217  eqrabi  38504  ecres  38533  dfdm6  38555  ruvALT  43024  rp-abid  43732  dfuniv2  44655  compeq  44792  dfnrm2  49288  dfnrm3  49289  dftermc2  49876  dftermc3  49887