Theorem abeq2i 2189

Description: Equality of a class variable and a class abstraction (inference rule). (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 2145	. 2 |- ( x e. A <-> x e. { x | ph } )
3		abid 2069	. 2 |- ( x e. { x | ph } <-> ph )
4	2, 3	bitri 182	1 |- ( x e. A <-> ph )

Syntax hints:   <-> wb 103   = wceq 1284   e. wcel 1433   {cab 2067

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077

This theorem is referenced by:  rabid  2529  vex  2604  csbco  2917  csbnestgf  2954  pwss  3397  snsspw  3556  iunpw  4229  ordon  4230  funcnv3  4981  tfrlem4  5952  tfrlem8  5957  tfrlem9  5958  tfrlemibxssdm  5964  1idprl  6780  1idpru  6781  recexprlem1ssl  6823  recexprlem1ssu  6824  recexprlemss1l  6825  recexprlemss1u  6826