Theorem abeq2i 2584

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
abeqi.1

Assertion

Ref	Expression
abeq2i

Proof of Theorem abeq2i

Step	Hyp	Ref	Expression
1		abeqi.1	. . . 4
2	1	a1i 11	. . 3
3	2	abeq2d 2583	. 2
4	3	trud 1404	1

Syntax hints:  <->wb 184  =wceq 1395  wtru 1396  e.wcel 1818  {cab 2442

This theorem is referenced by:  abeq1i  2586  rabid  3034  vex  3112  csbco  3444  csbnestgf  3840  elsn  4043  funcnv3  5654  opabiota  5936  zfrep6  6768  tfrlem4  7067  tfrlem8  7072  tfrlem9  7073  ixpn0  7521  mapsnen  7613  sbthlem1  7647  dffi3  7911  1idpr  9428  ltexprlem1  9435  ltexprlem2  9436  ltexprlem3  9437  ltexprlem4  9438  ltexprlem6  9440  ltexprlem7  9441  reclem2pr  9447  reclem3pr  9448  reclem4pr  9449  supsrlem  9509  dissnref  20029  dissnlocfin  20030  txbas  20068  xkoccn  20120  xkoptsub  20155  xkoco1cn  20158  xkoco2cn  20159  xkoinjcn  20188  mbfi1fseqlem4  22125  avril1  25171  rnmpt2ss  27515  setinds  29210  wfrlem2  29344  wfrlem3  29345  wfrlem4  29346  wfrlem9  29351  frrlem2  29388  frrlem3  29389  frrlem4  29390  frrlem5e  29395  frrlem11  29399  sdclem1  30236  csbcom2fi  30534  csbgfi  30535  bnj1436  33898  bnj916  33991  bnj983  34009  bnj1083  34034  bnj1245  34070  bnj1311  34080  bnj1371  34085  bnj1398  34090  bj-ififc  34166  bj-elsngl  34526  bj-projun  34552  bj-projval  34554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452