Theorem abeq2i 2950

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

Syntax hints:   ↔ wb 208   = wceq 1537  ⊤wtru 1538   ∈ wcel 2114  {cab 2801

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895

This theorem is referenced by:  abeq1i  2951  rabid  3380  vexOLD  3500  csbcow  3900  csbco  3901  csbgfi  3905  csbnestgfw  4373  csbnestgf  4378  ssrel  5659  relopabi  5696  cnv0  6001  funcnv3  6426  opabiota  6748  zfrep6  7658  wfrlem2  7957  wfrlem3  7958  wfrlem4  7960  wfrdmcl  7965  tfrlem4  8017  tfrlem8  8022  tfrlem9  8023  ixpn0  8496  sbthlem1  8629  dffi3  8897  1idpr  10453  ltexprlem1  10460  ltexprlem2  10461  ltexprlem3  10462  ltexprlem4  10463  ltexprlem6  10465  ltexprlem7  10466  reclem2pr  10472  reclem3pr  10473  reclem4pr  10474  supsrlem  10535  dissnref  22138  dissnlocfin  22139  txbas  22177  xkoccn  22229  xkoptsub  22264  xkoco1cn  22267  xkoco2cn  22268  xkoinjcn  22297  mbfi1fseqlem4  24321  avril1  28244  rnmposs  30421  bnj1436  32113  bnj916  32207  bnj983  32225  bnj1083  32252  bnj1245  32288  bnj1311  32298  bnj1371  32303  bnj1398  32308  setinds  33025  frrlem2  33126  frrlem3  33127  frrlem4  33128  frrlem8  33132  bj-elsngl  34282  bj-projun  34308  bj-projval  34310  f1omptsnlem  34619  icoreresf  34635  finxp0  34674  finxp1o  34675  finxpsuclem  34680  sdclem1  35020  csbcom2fi  35408