Theorem abbi2i 2322

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

Syntax hints:   <-> wb 105   = wceq 1373   e. wcel 2178   {cab 2193

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203

This theorem is referenced by:  abid2  2328  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  symdifxor  3447  dfnul2  3470  dfpr2  3662  dftp2  3692  0iin  4000  pwpwab  4029  epse  4407  fv3  5622  fo1st  6266  fo2nd  6267  xp2  6282  tfrlem3  6420  tfr1onlem3  6447  mapsn  6800  ixpconstg  6817  ixp0x  6836  nnzrab  9431  nn0zrab  9432