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  7327  supeq2  7330  supeq3  7331  cardcl  7527  isnumi  7528  cardval3ex  7531  carden2bex  7536  genpdflem  7875  genipv  7877  genpelxp  7879  addcomprg  7946  mulcomprg  7948  uzval  9933  ixxval  10309  fzval  10424  hashinfom  11233  hashennn  11235  ssenneg  11296  hashfibclem  11298  hashfibc  11299  shftfn  11605  bitsfval  12728  gcdval  12755  lcmval  12860  isprm  12906  odzval  13043  pceulem  13096  pceu  13097  pcval  13098  pczpre  13099  pcdiv  13104  ballotfilemi  13295  ballotfi  13334  cntzval  14147  cntzsnval  14150  lspval  14811  aspval  15099  psrmulvalfi  15160  istopon  15205  toponsspwpwg  15214  clsval  15303  neival  15335  cnpval  15390  blvalps  15580  blval  15581  limccl  15851  ellimc3apf  15852  eldvap  15874  sgmval  16213  vtxdgfifival  16698  clwwlknon  16836  clwwlk0on0  16838  eupth2fi  16886