Theorem abeq2i 2722

Description: Equality of a class variable and a class abstraction (inference rule). (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 2721	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	trud 1484	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 195   = wceq 1475  ⊤wtru 1476   ∈ wcel 1977  {cab 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606

This theorem is referenced by:  abeq1i  2723  rabid  3095  vex  3176  csbco  3509  csbnestgf  3948  ssrel  5130  relopabi  5167  cnv0  5454  funcnv3  5873  opabiota  6171  zfrep6  7027  wfrlem2  7302  wfrlem3  7303  wfrlem4  7305  wfrdmcl  7310  tfrlem4  7362  tfrlem8  7367  tfrlem9  7368  ixpn0  7826  mapsnen  7920  sbthlem1  7955  dffi3  8220  1idpr  9730  ltexprlem1  9737  ltexprlem2  9738  ltexprlem3  9739  ltexprlem4  9740  ltexprlem6  9742  ltexprlem7  9743  reclem2pr  9749  reclem3pr  9750  reclem4pr  9751  supsrlem  9811  dissnref  21141  dissnlocfin  21142  txbas  21180  xkoccn  21232  xkoptsub  21267  xkoco1cn  21270  xkoco2cn  21271  xkoinjcn  21300  mbfi1fseqlem4  23291  avril1  26711  rnmpt2ss  28856  bnj1436  30164  bnj916  30257  bnj983  30275  bnj1083  30300  bnj1245  30336  bnj1311  30346  bnj1371  30351  bnj1398  30356  setinds  30927  frrlem2  31025  frrlem3  31026  frrlem4  31027  frrlem5e  31032  frrlem11  31036  bj-ififc  31736  bj-elsngl  32149  bj-projun  32175  bj-projval  32177  f1omptsnlem  32359  icoreresf  32376  finxp0  32404  finxp1o  32405  finxpsuclem  32410  sdclem1  32709  csbcom2fi  33104  csbgfi  33105