Theorem rabbidv 2791

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)

Hypothesis

Ref	Expression
rabbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
rabbidv	|- ( ph -> { x e. A | ps } = { x e. A | ch } )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem rabbidv

Step	Hyp	Ref	Expression
1		rabbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 276	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	rabbidva 2790	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   e. wcel 2202   {crab 2514

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-ral 2515  df-rab 2519

This theorem is referenced by:  rabeqbidv  2797  difeq2  3319  seex  4432  mptiniseg  5231  elovmporab  6222  supeq1  7185  supeq2  7188  supeq3  7189  cardcl  7385  isnumi  7386  cardval3ex  7389  carden2bex  7394  genpdflem  7727  genipv  7729  genpelxp  7731  addcomprg  7798  mulcomprg  7800  uzval  9757  ixxval  10131  fzval  10245  hashinfom  11041  hashennn  11043  shftfn  11402  bitsfval  12521  gcdval  12548  lcmval  12653  isprm  12699  odzval  12832  pceulem  12885  pceu  12886  pcval  12887  pczpre  12888  pcdiv  12893  lspval  14423  istopon  14756  toponsspwpwg  14765  clsval  14854  neival  14886  cnpval  14941  blvalps  15131  blval  15132  limccl  15402  ellimc3apf  15403  eldvap  15425  sgmval  15726  vtxdgfifival  16161  clwwlknon  16299  clwwlk0on0  16301  eupth2fi  16349