Theorem abeq2i 2915

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

Syntax hints:   ↔ wb 207   = wceq 1520  ⊤wtru 1521   ∈ wcel 2079  {cab 2773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1523  df-ex 1760  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861

This theorem is referenced by:  abeq1i  2916  rabid  3334  vexOLD  3436  csbco  3820  csbgfi  3824  csbnestgf  4285  ssrel  5535  relopabi  5572  cnv0  5867  funcnv3  6286  opabiota  6605  zfrep6  7503  wfrlem2  7797  wfrlem3  7798  wfrlem4  7800  wfrlem4OLD  7801  wfrdmcl  7806  tfrlem4  7858  tfrlem8  7863  tfrlem9  7864  ixpn0  8332  sbthlem1  8464  dffi3  8731  1idpr  10286  ltexprlem1  10293  ltexprlem2  10294  ltexprlem3  10295  ltexprlem4  10296  ltexprlem6  10298  ltexprlem7  10299  reclem2pr  10305  reclem3pr  10306  reclem4pr  10307  supsrlem  10368  dissnref  21808  dissnlocfin  21809  txbas  21847  xkoccn  21899  xkoptsub  21934  xkoco1cn  21937  xkoco2cn  21938  xkoinjcn  21967  mbfi1fseqlem4  23990  avril1  27921  rnmposs  30082  bnj1436  31684  bnj916  31777  bnj983  31795  bnj1083  31820  bnj1245  31856  bnj1311  31866  bnj1371  31871  bnj1398  31876  setinds  32576  frrlem2  32678  frrlem3  32679  frrlem4  32680  frrlem8  32684  bj-ififc  33465  bj-elsngl  33831  bj-projun  33857  bj-projval  33859  f1omptsnlem  34094  icoreresf  34110  finxp0  34149  finxp1o  34150  finxpsuclem  34155  sdclem1  34496  csbcom2fi  34886