Theorem rabid2 2683

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 2314	. . 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 1493	. . 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 2493	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
6	5	eqeq2i 2216	. 2 |- ( A = { x e. A | ph } <-> A = { x | ( x e. A /\ ph ) } )
7		df-ral 2489	. 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 1371   = wceq 1373   e. wcel 2176   {cab 2191   A.wral 2484   {crab 2488

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-ral 2489  df-rab 2493

This theorem is referenced by:  rabxmdc  3492  rabrsndc  3701  class2seteq  4207  dmmptg  5180  dmmptd  5406  fneqeql  5688  fmpt  5730  acexmidlemph  5937  inffiexmid  7003  ssfirab  7033  exmidaclem  7320  ioomax  10070  iccmax  10071  dfphi2  12542  phiprmpw  12544  phisum  12563  unennn  12768  znnen  12769  isnsg4  13548  lssuni  14125  psrbagfi  14435  lgsquadlem2  15555