Theorem abeq2i 1570

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 1538	. 2 |- (x e. A <-> x e. {x | ph})
3		abid 1465	. 2 |- (x e. {x | ph} <-> ph)
4	2, 3	bitr 173	1 |- (x e. A <-> ph)

Syntax hints:   <-> wb 146   = wceq 956   e. wcel 958  {cab 1463

This theorem is referenced by:  rabid 1769  visset 1813  csbcog 2007  noel 2284  elpw 2404  elsn 2421  pw0 2468  snsspw 2479  elopab 2811  iunpw 2914  funcnv3 3558  zfrep6 3614  fv2 3720  tz6.12-1 3736  fopab2 3823  tfrlem4 3914  tfrlem5 3915  tfrlem8 3918  tfrlem9 3919  mapsnen 4429  sbthlem1 4447  ac6lem 4754  1pr 5117  1idpr 5133  ltexprlem1 5142  ltexprlem2 5143  ltexprlem3 5144  ltexprlem4 5145  ltexprlem6 5147  ltexprlem7 5148  reclem1pr 5156  reclem2pr 5157  reclem3pr 5158  reclem4pr 5159  suppsrlem 5221  suppsr3 5224  suprelem 5259  isbasis2g 7612  avril1 8784  chsscm 9112  chcmh 9113

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472

Copyright terms: Public domain