Theorem eqabi 2863

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  abid1  2864  cbvralcsf  3904  cbvreucsf  3906  cbvrabcsf  3907  dfsymdif4  4222  dfsymdif2  4224  dfpr2  4610  dftp2  4655  iunid  5024  0iin  5028  pwpwab  5067  epse  5620  pwvabrel  5689  fv3  6876  fo1st  7988  fo2nd  7989  xp2  8005  tfrlem3  8346  ixpconstg  8879  ixp0x  8899  ruv  9555  dfom4  9602  cardnum  10047  alephiso  10051  nnzrab  12561  nn0zrab  12562  qnnen  16181  bdayfo  27589  madeval2  27761  h2hcau  30908  dfch2  31336  hhcno  31833  hhcnf  31834  pjhmopidm  32112  fobigcup  35888  dfsingles2  35909  dfrecs2  35938  dfrdg4  35939  dfint3  35940  bj-snglinv  36960  ecres  38267  dfdm6  38289  ruvALT  42657  rp-abid  43367  dfuniv2  44291  compeq  44429  dfnrm2  48920  dfnrm3  48921  dftermc2  49509  dftermc3  49520