Theorem rabid2 2721

Description: An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
rabid2	|- ( A = { x e. A | ph } <-> A. x e. A ph )

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem rabid2

Step	Hyp	Ref	Expression
1		abeq2 2341	. . 3 |- ( A = { x | ( x e. A /\ ph ) } <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) )
2		pm4.71 389	. . . 4 |- ( ( x e. A -> ph ) <-> ( x e. A <-> ( x e. A /\ ph ) ) )
3	2	albii 1519	. . 3 |- ( A. x ( x e. A -> ph ) <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) )
4	1, 3	bitr4i 187	. 2 |- ( A = { x | ( x e. A /\ ph ) } <-> A. x ( x e. A -> ph ) )
5		df-rab 2529	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
6	5	eqeq2i 2243	. 2 |- ( A = { x e. A | ph } <-> A = { x | ( x e. A /\ ph ) } )
7		df-ral 2525	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
8	4, 6, 7	3bitr4i 212	1 |- ( A = { x e. A | ph } <-> A. x e. A ph )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1396   = wceq 1398   e. wcel 2203   {cab 2218   A.wral 2520   {crab 2524

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-ral 2525  df-rab 2529

This theorem is referenced by:  rabxmdc  3540  rabrsndc  3759  class2seteq  4276  dmmptg  5260  dmmptd  5489  fneqeql  5786  fmpt  5827  acexmidlemph  6043  inffiexmid  7166  ssfirab  7197  exmidaclem  7515  ioomax  10281  iccmax  10282  hashfibc  11207  dfphi2  12917  phiprmpw  12919  phisum  12938  unennn  13148  znnen  13149  isnsg4  13929  lssuni  14511  psrbagfi  14823  lgsquadlem2  15951