Theorem abeq2i 2286

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

Syntax hints:   <-> wb 105   = wceq 1353   e. wcel 2146   {cab 2161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171

This theorem is referenced by:  rabid  2650  vex  2738  csbco  3065  csbcow  3066  csbnestgf  3107  ifmdc  3571  pwss  3588  snsspw  3760  iunpw  4474  ordon  4479  funcnv3  5270  tfrlem4  6304  tfrlem8  6309  tfrlem9  6310  tfrlemibxssdm  6318  tfr1onlembxssdm  6334  tfrcllembxssdm  6347  ixpm  6720  mapsnen  6801  sbthlem1  6946  1idprl  7564  1idpru  7565  recexprlem1ssl  7607  recexprlem1ssu  7608  recexprlemss1l  7609  recexprlemss1u  7610  txbas  13338