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 } )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209   {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-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-ral 2533  df-rab 2537

This theorem is used by:  rabeqbidv  2816  difeq2  3341  seex  4480  mptiniseg  5282  elovmporab  6289  supeq1  7326  supeq2  7329  supeq3  7330  cardcl  7526  isnumi  7527  cardval3ex  7530  carden2bex  7535  genpdflem  7874  genipv  7876  genpelxp  7878  addcomprg  7945  mulcomprg  7947  uzval  9923  ixxval  10298  fzval  10413  hashinfom  11217  hashennn  11219  ssenneg  11280  hashfibclem  11282  hashfibc  11283  shftfn  11589  bitsfval  12709  gcdval  12736  lcmval  12841  isprm  12887  odzval  13020  pceulem  13073  pceu  13074  pcval  13075  pczpre  13076  pcdiv  13081  ballotfilemi  13243  ballotfi  13282  lspval  14727  aspval  15015  istopon  15114  toponsspwpwg  15123  clsval  15212  neival  15244  cnpval  15299  blvalps  15489  blval  15490  limccl  15760  ellimc3apf  15761  eldvap  15783  sgmval  16097  vtxdgfifival  16532  clwwlknon  16670  clwwlk0on0  16672  eupth2fi  16720