Theorem abbi2i 2345

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 2339	. 2 |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )
2		abbiri.1	. 2 |- ( x e. A <-> ph )
3	1, 2	mpgbir 1501	1 |- A = { x | ph }

Syntax hints:   <-> wb 105   = wceq 1397   e. wcel 2201   {cab 2216

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226

This theorem is referenced by:  abid2  2351  cbvralcsf  3189  cbvrexcsf  3190  cbvreucsf  3191  cbvrabcsf  3192  symdifxor  3472  dfnul2  3495  dfpr2  3689  dftp2  3719  0iin  4030  pwpwab  4059  epse  4441  fv3  5665  fo1st  6325  fo2nd  6326  xp2  6341  tfrlem3  6482  tfr1onlem3  6509  mapsn  6864  ixpconstg  6881  ixp0x  6900  nnzrab  9508  nn0zrab  9509