Theorem eqabi 2871

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 2869	. 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
4	3	mptru 1548	1 ⊢ 𝐴 = {𝑥 ∣ 𝜑}

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  abid1  2872  cbvralcsf  3891  cbvreucsf  3893  cbvrabcsf  3894  dfsymdif4  4211  dfsymdif2  4213  dfpr2  4601  dftp2  4648  iunid  5016  0iin  5019  pwpwab  5058  epse  5606  pwvabrel  5675  fv3  6852  fo1st  7953  fo2nd  7954  xp2  7970  tfrlem3  8309  ixpconstg  8844  ixp0x  8864  ruv  9510  dfom4  9558  cardnum  10004  alephiso  10008  nnzrab  12519  nn0zrab  12520  qnnen  16138  bdayfo  27645  madeval2  27829  h2hcau  31054  dfch2  31482  hhcno  31979  hhcnf  31980  pjhmopidm  32258  fobigcup  36092  dfsingles2  36113  dfrecs2  36144  dfrdg4  36145  dfint3  36146  bj-snglinv  37173  ecres  38478  dfdm6  38500  ruvALT  42912  rp-abid  43620  dfuniv2  44543  compeq  44680  dfnrm2  49177  dfnrm3  49178  dftermc2  49765  dftermc3  49776