Theorem eqabi 2875

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

Syntax hints:   ↔ wb 206   = wceq 1537  ⊤wtru 1538   ∈ wcel 2106  {cab 2712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814

This theorem is referenced by:  abid1  2876  cbvralcsf  3953  cbvreucsf  3955  cbvrabcsf  3956  dfsymdif4  4265  dfsymdif2  4267  dfpr2  4651  dftp2  4696  iunid  5065  0iin  5069  pwpwab  5108  epse  5671  pwvabrel  5740  fv3  6925  fo1st  8033  fo2nd  8034  xp2  8050  tfrlem3  8417  ixpconstg  8945  ixp0x  8965  ruv  9640  dfom4  9687  cardnum  10132  alephiso  10136  nnzrab  12643  nn0zrab  12644  qnnen  16246  bdayfo  27737  madeval2  27907  h2hcau  31008  dfch2  31436  hhcno  31933  hhcnf  31934  pjhmopidm  32212  fobigcup  35882  dfsingles2  35903  dfrecs2  35932  dfrdg4  35933  dfint3  35934  bj-snglinv  36955  ecres  38260  dfdm6  38283  ruvALT  42656  rp-abid  43368  dfuniv2  44298  compeq  44436  dfnrm2  48728  dfnrm3  48729