Theorem abeq2i 2001

Description: Equality of a class variable and a class abstraction (inference rule).

Hypothesis

Ref	Expression
abeqi.1	|- A = {x | ph}

Assertion

Ref	Expression
abeq2i	|- (x e. A <-> ph)

Proof of Theorem abeq2i

Step	Hyp	Ref	Expression
1		abeqi.1	. . 3 |- A = {x | ph}
2	1	eleq2i 1961	. 2 |- (x e. A <-> x e. {x | ph})
3		abid 1873	. 2 |- (x e. {x | ph} <-> ph)
4	2, 3	bitri 190	1 |- (x e. A <-> ph)

Syntax hints:   <-> wb 163   = wceq 1298   e. wcel 1300  {cab 1871

This theorem is referenced by:  rabid 2253  visset 2295  csbcog 2547  noel 2879  elpw 3037  pwss 3043  elsn 3058  pw0OLD 3133  snsspw 3149  elopab 3559  iunpw 3858  funcnv3 4476  zfrep6 4545  fv2OLD 4677  tz6.12-1 4693  fopab2 4796  tfrlem4 5122  tfrlem5 5123  tfrlem8 5126  tfrlem9 5127  mapsnen 5488  sbthlem1 5510  ac6lem 5916  1pr 6269  1idpr 6285  ltexprlem1 6294  ltexprlem2 6295  ltexprlem3 6296  ltexprlem4 6297  ltexprlem6 6299  ltexprlem7 6300  reclem1pr 6308  reclem2pr 6309  reclem3pr 6310  reclem4pr 6311  suppsrlem 6373  suppsr3 6376  suprelem 6411  isbasis2g 8881  grothpw 10134  avril1 10142  fipreima 10175  chsscmi 10745  chcmhi 10746  bnj1436 13130  bnj902 13326  bnj894 13327  bnj916 13332  bnj983 13357  bnj1083 13408  bnj1244 13461  bnj1245 13463  bnj1255 13466  bnj1258 13468  bnj1371 13505  bnj1398 13515  setinds 13844  wfrlem2 13958  wfrlem3 13959  wfrlem4 13960  wfrlem9 13965  wfrlem12 13968  fopab2g 14485  eroprlem 15732  eropreu 15733  fipreimaOLD 15756  strdif 16719  psubspset 17225  psubclset 17346

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880

Copyright terms: Public domain