Theorem eqabi 2868

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

Syntax hints:   ↔ wb 206   = wceq 1541  ⊤wtru 1542   ∈ wcel 2113  {cab 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808

This theorem is referenced by:  abid1  2869  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  dfsymdif4  4208  dfsymdif2  4210  dfpr2  4598  dftp2  4645  iunid  5013  0iin  5016  pwpwab  5055  epse  5603  pwvabrel  5672  fv3  6848  fo1st  7949  fo2nd  7950  xp2  7966  tfrlem3  8305  ixpconstg  8838  ixp0x  8858  ruv  9500  dfom4  9548  cardnum  9994  alephiso  9998  nnzrab  12508  nn0zrab  12509  qnnen  16126  bdayfo  27619  madeval2  27797  h2hcau  30963  dfch2  31391  hhcno  31888  hhcnf  31889  pjhmopidm  32167  fobigcup  35965  dfsingles2  35986  dfrecs2  36017  dfrdg4  36018  dfint3  36019  bj-snglinv  37039  ecres  38340  dfdm6  38362  ruvALT  42790  rp-abid  43498  dfuniv2  44422  compeq  44559  dfnrm2  49059  dfnrm3  49060  dftermc2  49648  dftermc3  49659