Theorem abeq2i 1617

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 1585	. 2 |- (x e. A <-> x e. {x | ph})
3		abid 1511	. 2 |- (x e. {x | ph} <-> ph)
4	2, 3	bitri 180	1 |- (x e. A <-> ph)

Syntax hints:   <-> wb 153   = wceq 997   e. wcel 999  {cab 1509

This theorem is referenced by:  rabid 1816  visset 1860  csbcog 2058  noel 2335  elpw 2456  elsn 2473  pw0 2522  snsspw 2533  elopab 2867  iunpw 2971  funcnv3 3615  zfrep6 3671  fv2 3777  tz6.12-1 3793  fopab2 3880  tfrlem4 3972  tfrlem5 3973  tfrlem8 3976  tfrlem9 3977  mapsnen 4490  sbthlem1 4510  ac6lem 4816  1pr 5182  1idpr 5198  ltexprlem1 5207  ltexprlem2 5208  ltexprlem3 5209  ltexprlem4 5210  ltexprlem6 5212  ltexprlem7 5213  reclem1pr 5221  reclem2pr 5222  reclem3pr 5223  reclem4pr 5224  suppsrlem 5286  suppsr3 5289  suprelem 5324  isbasis2g 7701  avril1 8867  chsscmi 9195  chcmhi 9196

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518

Copyright terms: Public domain