Theorem abbi2i 2281

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
abbiri.1	|- ( x e. A <-> ph )

Assertion

Ref	Expression
abbi2i	|- A = { x | ph }

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem abbi2i

Step	Hyp	Ref	Expression
1		abeq2 2275	. 2 |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )
2		abbiri.1	. 2 |- ( x e. A <-> ph )
3	1, 2	mpgbir 1441	1 |- A = { x | ph }

Syntax hints:   <-> wb 104   = wceq 1343   e. wcel 2136   {cab 2151

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161

This theorem is referenced by:  abid2  2287  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  symdifxor  3388  dfnul2  3411  dfpr2  3595  dftp2  3625  0iin  3924  pwpwab  3953  epse  4320  fv3  5509  fo1st  6125  fo2nd  6126  xp2  6141  tfrlem3  6279  tfr1onlem3  6306  mapsn  6656  ixpconstg  6673  ixp0x  6692  nnzrab  9215  nn0zrab  9216