Theorem rabbidv 2810

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 2809	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209   {crab 2532

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 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 theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-ral 2533  df-rab 2537

This theorem is referenced by:  rabeqbidv  2816  difeq2  3341  seex  4475  mptiniseg  5277  elovmporab  6279  supeq1  7316  supeq2  7319  supeq3  7320  cardcl  7516  isnumi  7517  cardval3ex  7520  carden2bex  7525  genpdflem  7864  genipv  7866  genpelxp  7868  addcomprg  7935  mulcomprg  7937  uzval  9902  ixxval  10277  fzval  10392  hashinfom  11195  hashennn  11197  ssenneg  11258  hashfibclem  11260  hashfibc  11261  shftfn  11567  bitsfval  12687  gcdval  12714  lcmval  12819  isprm  12865  odzval  12998  pceulem  13051  pceu  13052  pcval  13053  pczpre  13054  pcdiv  13059  ballotfilemi  13221  ballotfi  13260  lspval  14699  istopon  15037  toponsspwpwg  15046  clsval  15135  neival  15167  cnpval  15222  blvalps  15412  blval  15413  limccl  15683  ellimc3apf  15684  eldvap  15706  sgmval  16011  vtxdgfifival  16446  clwwlknon  16584  clwwlk0on0  16586  eupth2fi  16634