Theorem abeq2i 2874

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) (Proof shortened by Wolf Lammen, 15-Nov-2019.)

Hypothesis

Ref	Expression
abeq2i.1	⊢ 𝐴 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
abeq2i	⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Proof of Theorem abeq2i

Step	Hyp	Ref	Expression
1		abeq2i.1	. . . 4 ⊢ 𝐴 = {𝑥 ∣ 𝜑}
2	1	a1i 11	. . 3 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
3	2	abeq2d 2873	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	mptru 1547	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 205   = wceq 1540  ⊤wtru 1541   ∈ wcel 2105  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-12 2170  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815

This theorem is referenced by:  abeq1i  2875  rabid  3422  csbcow  3856  csbco  3857  csbgfi  3862  csbnestgfw  4363  csbnestgf  4368  ssrelOLD  5710  relopabi  5749  cnv0  6064  funcnv3  6538  opabiota  6888  zfrep6  7840  frrlem2  8148  frrlem3  8149  frrlem4  8150  frrlem8  8154  fprresex  8171  wfrlem2OLD  8185  wfrlem3OLD  8186  wfrlem4OLD  8188  wfrdmclOLD  8193  tfrlem4  8255  tfrlem8  8260  tfrlem9  8261  ixpn0  8764  sbthlem1  8923  dffi3  9258  1idpr  10855  ltexprlem1  10862  ltexprlem2  10863  ltexprlem3  10864  ltexprlem4  10865  ltexprlem6  10867  ltexprlem7  10868  reclem2pr  10874  reclem3pr  10875  reclem4pr  10876  supsrlem  10937  dissnref  22750  dissnlocfin  22751  txbas  22789  xkoccn  22841  xkoptsub  22876  xkoco1cn  22879  xkoco2cn  22880  xkoinjcn  22909  mbfi1fseqlem4  24954  avril1  28935  rnmposs  31119  bnj1436  32925  bnj916  33019  bnj983  33037  bnj1083  33064  bnj1245  33100  bnj1311  33110  bnj1371  33115  bnj1398  33120  setinds  33856  bj-elsngl  35218  bj-projun  35244  bj-projval  35246  f1omptsnlem  35567  icoreresf  35583  finxp0  35622  finxp1o  35623  finxpsuclem  35628  sdclem1  35961  csbcom2fi  36346  rr-grothshortbi  42149  upwordisword  46775  tworepnotupword  46780