Theorem abeq2i 2721

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 2720	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	trud 1483	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 194   = wceq 1474  ⊤wtru 1475   ∈ wcel 1976  {cab 2595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605

This theorem is referenced by:  abeq1i  2722  rabid  3094  vex  3175  csbco  3508  csbnestgf  3947  funcnv3  5859  opabiota  6156  zfrep6  7004  wfrlem2  7279  wfrlem3  7280  wfrlem4  7282  wfrdmcl  7287  tfrlem4  7339  tfrlem8  7344  tfrlem9  7345  ixpn0  7803  mapsnen  7897  sbthlem1  7932  dffi3  8197  1idpr  9707  ltexprlem1  9714  ltexprlem2  9715  ltexprlem3  9716  ltexprlem4  9717  ltexprlem6  9719  ltexprlem7  9720  reclem2pr  9726  reclem3pr  9727  reclem4pr  9728  supsrlem  9788  dissnref  21083  dissnlocfin  21084  txbas  21122  xkoccn  21174  xkoptsub  21209  xkoco1cn  21212  xkoco2cn  21213  xkoinjcn  21242  mbfi1fseqlem4  23208  avril1  26477  rnmpt2ss  28662  bnj1436  29970  bnj916  30063  bnj983  30081  bnj1083  30106  bnj1245  30142  bnj1311  30152  bnj1371  30157  bnj1398  30162  setinds  30733  frrlem2  30831  frrlem3  30832  frrlem4  30833  frrlem5e  30838  frrlem11  30842  bj-ififc  31542  bj-elsngl  31945  bj-projun  31971  bj-projval  31973  f1omptsnlem  32155  icoreresf  32172  finxp0  32200  finxp1o  32201  finxpsuclem  32206  sdclem1  32505  csbcom2fi  32900  csbgfi  32901