Theorem abeq2i 2198

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.)

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

Syntax hints:   <-> wb 103   = wceq 1289   e. wcel 1438   {cab 2074

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084

This theorem is referenced by:  rabid  2542  vex  2622  csbco  2942  csbnestgf  2980  ifmdc  3428  pwss  3445  snsspw  3608  iunpw  4302  ordon  4303  funcnv3  5076  tfrlem4  6078  tfrlem8  6083  tfrlem9  6084  tfrlemibxssdm  6092  tfr1onlembxssdm  6108  tfrcllembxssdm  6121  mapsnen  6526  sbthlem1  6664  1idprl  7147  1idpru  7148  recexprlem1ssl  7190  recexprlem1ssu  7191  recexprlemss1l  7192  recexprlemss1u  7193