Theorem abbi2i 2308

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

Syntax hints:   <-> wb 105   = wceq 1364   e. wcel 2164   {cab 2179

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189

This theorem is referenced by:  abid2  2314  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  symdifxor  3426  dfnul2  3449  dfpr2  3638  dftp2  3668  0iin  3972  pwpwab  4001  epse  4374  fv3  5578  fo1st  6212  fo2nd  6213  xp2  6228  tfrlem3  6366  tfr1onlem3  6393  mapsn  6746  ixpconstg  6763  ixp0x  6782  nnzrab  9344  nn0zrab  9345