Theorem abeq2i 1573

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

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

This theorem is referenced by:  rabid 1772  visset 1816  csbcog 2010  noel 2287  elpw 2408  elsn 2425  pw0 2472  snsspw 2483  elopab 2817  iunpw 2920  funcnv3 3564  zfrep6 3620  fv2 3726  tz6.12-1 3742  fopab2 3829  tfrlem4 3920  tfrlem5 3921  tfrlem8 3924  tfrlem9 3925  mapsnen 4435  sbthlem1 4453  ac6lem 4764  1pr 5129  1idpr 5145  ltexprlem1 5154  ltexprlem2 5155  ltexprlem3 5156  ltexprlem4 5157  ltexprlem6 5159  ltexprlem7 5160  reclem1pr 5168  reclem2pr 5169  reclem3pr 5170  reclem4pr 5171  suppsrlem 5233  suppsr3 5236  suprelem 5271  isbasis2g 7611  avril1 8779  chsscm 9107  chcmh 9108

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475

Copyright terms: Public domain