Theorem eqabi 2877

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

Syntax hints:   ↔ wb 206   = wceq 1540  ⊤wtru 1541   ∈ wcel 2108  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816

This theorem is referenced by:  abid1  2878  cbvralcsf  3941  cbvreucsf  3943  cbvrabcsf  3944  dfsymdif4  4259  dfsymdif2  4261  dfpr2  4646  dftp2  4691  iunid  5060  0iin  5064  pwpwab  5103  epse  5667  pwvabrel  5736  fv3  6924  fo1st  8034  fo2nd  8035  xp2  8051  tfrlem3  8418  ixpconstg  8946  ixp0x  8966  ruv  9642  dfom4  9689  cardnum  10134  alephiso  10138  nnzrab  12645  nn0zrab  12646  qnnen  16249  bdayfo  27722  madeval2  27892  h2hcau  30998  dfch2  31426  hhcno  31923  hhcnf  31924  pjhmopidm  32202  fobigcup  35901  dfsingles2  35922  dfrecs2  35951  dfrdg4  35952  dfint3  35953  bj-snglinv  36973  ecres  38279  dfdm6  38302  ruvALT  42679  rp-abid  43391  dfuniv2  44321  compeq  44459  dfnrm2  48829  dfnrm3  48830  dftermc2  49150