Theorem eqabi 2896

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145  {cab 2739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is used by:  abid1  2897  cbvralcsf  3889  cbvreucsf  3891  cbvrabcsf  3892  dfsymdif4  4205  dfsymdif2  4207  dfpr2  4605  dftp2  4652  iunid  5019  0iin  5022  pwpwab  5063  epse  5633  pwvabrel  5702  fv3  6895  fo1st  8010  fo2nd  8011  xp2  8027  tfrlem3  8369  ixpconstg  8918  ixp0x  8938  ruv  9586  dfom4  9634  cardnum  10154  alephiso  10158  nnzrab  12705  nn0zrab  12706  qnnen  16361  bdayfo  28016  madeval2  28201  h2hcau  31563  dfch2  31991  hhcno  32488  hhcnf  32489  pjhmopidm  32767  fobigcup  36632  dfsingles2  36653  dfrecs2  36684  dfrdg4  36685  dfint3  36686  bj-snglinv  37855  eqrabi  39156  ecres  39185  dfdm6  39207  ruvALT  43634  rp-abid  44338  dfuniv2  45245  compeq  45382  dfnrm2  49984  dfnrm3  49985  dftermc2  50572  dftermc3  50583