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  9932  ixxval  10308  fzval  10423  hashinfom  11231  hashennn  11233  ssenneg  11294  hashfibclem  11296  hashfibc  11297  shftfn  11603  bitsfval  12725  gcdval  12752  lcmval  12857  isprm  12903  odzval  13040  pceulem  13093  pceu  13094  pcval  13095  pczpre  13096  pcdiv  13101  ballotfilemi  13292  ballotfi  13331  lspval  14776  aspval  15064  istopon  15163  toponsspwpwg  15172  clsval  15261  neival  15293  cnpval  15348  blvalps  15538  blval  15539  limccl  15809  ellimc3apf  15810  eldvap  15832  sgmval  16164  vtxdgfifival  16630  clwwlknon  16768  clwwlk0on0  16770  eupth2fi  16818