Theorem eqabi 2869

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

Syntax hints:   ↔ wb 205   = wceq 1541  ⊤wtru 1542   ∈ wcel 2106  {cab 2709

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810

This theorem is referenced by:  abid1  2870  cbvralcsf  3938  cbvreucsf  3940  cbvrabcsf  3941  dfsymdif4  4248  dfsymdif2  4250  dfpr2  4647  dftp2  4693  iunid  5063  0iin  5067  pwpwab  5106  epse  5659  pwvabrel  5727  fv3  6909  fo1st  7994  fo2nd  7995  xp2  8011  tfrlem3  8377  ixpconstg  8899  ixp0x  8919  ruv  9596  dfom4  9643  cardnum  10088  alephiso  10092  nnzrab  12589  nn0zrab  12590  qnnen  16155  bdayfo  27177  madeval2  27345  h2hcau  30227  dfch2  30655  hhcno  31152  hhcnf  31153  pjhmopidm  31431  fobigcup  34867  dfsingles2  34888  dfrecs2  34917  dfrdg4  34918  dfint3  34919  bj-snglinv  35848  ecres  37141  dfdm6  37165  ruvALT  41023  rp-abid  42118  dfuniv2  43051  compeq  43189  dfnrm2  47554  dfnrm3  47555