Theorem rabid2 2729

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 2347	. . 3 |- ( A = { x | ( x e. A /\ ph ) } <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) )
2		pm4.71 393	. . . 4 |- ( ( x e. A -> ph ) <-> ( x e. A <-> ( x e. A /\ ph ) ) )
3	2	albii 1523	. . 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 2537	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
6	5	eqeq2i 2249	. 2 |- ( A = { x e. A | ph } <-> A = { x | ( x e. A /\ ph ) } )
7		df-ral 2533	. 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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1400   = wceq 1402   e. wcel 2209   {cab 2224   A.wral 2528   {crab 2532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-ral 2533  df-rab 2537

This theorem is used by:  rabxmdc  3554  rabrsndc  3779  class2seteq  4300  dmmptg  5285  dmmptd  5514  fneqeql  5817  fmpt  5858  acexmidlemph  6078  inffiexmid  7213  ssfirab  7244  exmidaclem  7564  ioomax  10350  iccmax  10351  hashfibc  11283  dfphi2  12998  phiprmpw  13000  phisum  13019  unennn  13288  znnen  13289  isnsg4  14015  lssuni  14700  psrbagfi  15059  lgsquadlem2  16197  rabid1o  17034  stnot  17039