Theorem abeq2i 2876

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 2875	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	mptru 1548	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817

This theorem is referenced by:  abeq1i  2877  rabid  3308  csbcow  3851  csbco  3852  csbgfi  3857  csbnestgfw  4358  csbnestgf  4363  ssrel  5691  relopabi  5729  cnv0  6041  funcnv3  6500  opabiota  6845  zfrep6  7784  frrlem2  8087  frrlem3  8088  frrlem4  8089  frrlem8  8093  fprresex  8110  wfrlem2OLD  8124  wfrlem3OLD  8125  wfrlem4OLD  8127  wfrdmclOLD  8132  tfrlem4  8194  tfrlem8  8199  tfrlem9  8200  ixpn0  8692  sbthlem1  8839  dffi3  9151  1idpr  10769  ltexprlem1  10776  ltexprlem2  10777  ltexprlem3  10778  ltexprlem4  10779  ltexprlem6  10781  ltexprlem7  10782  reclem2pr  10788  reclem3pr  10789  reclem4pr  10790  supsrlem  10851  dissnref  22660  dissnlocfin  22661  txbas  22699  xkoccn  22751  xkoptsub  22786  xkoco1cn  22789  xkoco2cn  22790  xkoinjcn  22819  mbfi1fseqlem4  24864  avril1  28806  rnmposs  30990  bnj1436  32798  bnj916  32892  bnj983  32910  bnj1083  32937  bnj1245  32973  bnj1311  32983  bnj1371  32988  bnj1398  32993  setinds  33733  bj-elsngl  35137  bj-projun  35163  bj-projval  35165  f1omptsnlem  35486  icoreresf  35502  finxp0  35541  finxp1o  35542  finxpsuclem  35547  sdclem1  35880  csbcom2fi  36265  rr-grothshortbi  41874  upwordisword  46465