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  3930  cbvreucsf  3932  cbvrabcsf  3933  dfsymdif4  4243  dfsymdif2  4245  dfpr2  4644  dftp2  4689  iunid  5058  0iin  5062  pwpwab  5101  epse  5655  pwvabrel  5723  fv3  6909  fo1st  8009  fo2nd  8010  xp2  8026  tfrlem3  8395  ixpconstg  8921  ixp0x  8941  ruv  9623  dfom4  9670  cardnum  10115  alephiso  10119  nnzrab  12618  nn0zrab  12619  qnnen  16187  bdayfo  27626  madeval2  27796  h2hcau  30831  dfch2  31259  hhcno  31756  hhcnf  31757  pjhmopidm  32035  fobigcup  35552  dfsingles2  35573  dfrecs2  35602  dfrdg4  35603  dfint3  35604  bj-snglinv  36507  ecres  37805  dfdm6  37828  ruvALT  42157  rp-abid  42871  dfuniv2  43803  compeq  43941  dfnrm2  48061  dfnrm3  48062

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

OSZAR »