Theorem abeq2i 2265

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

Syntax hints:   <-> wb 104   = wceq 1332   e. wcel 2125   {cab 2140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150

This theorem is referenced by:  rabid  2629  vex  2712  csbco  3037  csbcow  3038  csbnestgf  3079  ifmdc  3538  pwss  3555  snsspw  3723  iunpw  4434  ordon  4439  funcnv3  5225  tfrlem4  6250  tfrlem8  6255  tfrlem9  6256  tfrlemibxssdm  6264  tfr1onlembxssdm  6280  tfrcllembxssdm  6293  ixpm  6664  mapsnen  6745  sbthlem1  6890  1idprl  7489  1idpru  7490  recexprlem1ssl  7532  recexprlem1ssu  7533  recexprlemss1l  7534  recexprlemss1u  7535  txbas  12597