Theorem eqabi 2871

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2163. (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 1549	1 ⊢ 𝐴 = {𝑥 ∣ 𝜑}

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  abid1  2872  cbvralcsf  3879  cbvreucsf  3881  cbvrabcsf  3882  dfsymdif4  4199  dfsymdif2  4201  dfpr2  4588  dftp2  4635  iunid  5003  0iin  5006  pwpwab  5045  epse  5613  pwvabrel  5682  fv3  6858  fo1st  7962  fo2nd  7963  xp2  7979  tfrlem3  8317  ixpconstg  8854  ixp0x  8874  ruv  9522  dfom4  9570  cardnum  10016  alephiso  10020  nnzrab  12555  nn0zrab  12556  qnnen  16180  bdayfo  27641  madeval2  27825  h2hcau  31050  dfch2  31478  hhcno  31975  hhcnf  31976  pjhmopidm  32254  fobigcup  36080  dfsingles2  36101  dfrecs2  36132  dfrdg4  36133  dfint3  36134  bj-snglinv  37279  eqrabi  38577  ecres  38606  dfdm6  38628  ruvALT  43102  rp-abid  43806  dfuniv2  44729  compeq  44866  dfnrm2  49407  dfnrm3  49408  dftermc2  49995  dftermc3  50006