Theorem eqabi 2861

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

Syntax hints:   ↔ wb 205   = wceq 1533  ⊤wtru 1534   ∈ wcel 2098  {cab 2702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802

This theorem is referenced by:  abid1  2862  cbvralcsf  3934  cbvreucsf  3936  cbvrabcsf  3937  dfsymdif4  4247  dfsymdif2  4249  dfpr2  4650  dftp2  4695  iunid  5064  0iin  5068  pwpwab  5107  epse  5661  pwvabrel  5729  fv3  6914  fo1st  8014  fo2nd  8015  xp2  8031  tfrlem3  8399  ixpconstg  8925  ixp0x  8945  ruv  9627  dfom4  9674  cardnum  10119  alephiso  10123  nnzrab  12623  nn0zrab  12624  qnnen  16193  bdayfo  27656  madeval2  27826  h2hcau  30861  dfch2  31289  hhcno  31786  hhcnf  31787  pjhmopidm  32065  fobigcup  35627  dfsingles2  35648  dfrecs2  35677  dfrdg4  35678  dfint3  35679  bj-snglinv  36582  ecres  37880  dfdm6  37903  ruvALT  42228  rp-abid  42949  dfuniv2  43881  compeq  44019  dfnrm2  48136  dfnrm3  48137

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »