Theorem abbi2i 2292

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

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173

This theorem is referenced by:  abid2  2298  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  symdifxor  3402  dfnul2  3425  dfpr2  3612  dftp2  3642  0iin  3946  pwpwab  3975  epse  4343  fv3  5539  fo1st  6158  fo2nd  6159  xp2  6174  tfrlem3  6312  tfr1onlem3  6339  mapsn  6690  ixpconstg  6707  ixp0x  6726  nnzrab  9277  nn0zrab  9278