Theorem eqabi 2872

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  abid1  2873  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  dfsymdif4  4200  dfsymdif2  4202  dfpr2  4589  dftp2  4636  iunid  5004  0iin  5007  pwpwab  5046  epse  5606  pwvabrel  5675  fv3  6852  fo1st  7955  fo2nd  7956  xp2  7972  tfrlem3  8310  ixpconstg  8847  ixp0x  8867  ruv  9513  dfom4  9561  cardnum  10007  alephiso  10011  nnzrab  12546  nn0zrab  12547  qnnen  16171  bdayfo  27655  madeval2  27839  h2hcau  31065  dfch2  31493  hhcno  31990  hhcnf  31991  pjhmopidm  32269  fobigcup  36096  dfsingles2  36117  dfrecs2  36148  dfrdg4  36149  dfint3  36150  bj-snglinv  37295  eqrabi  38591  ecres  38620  dfdm6  38642  ruvALT  43116  rp-abid  43824  dfuniv2  44747  compeq  44884  dfnrm2  49419  dfnrm3  49420  dftermc2  50007  dftermc3  50018