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  6221  supeq1  7184  supeq2  7187  supeq3  7188  cardcl  7384  isnumi  7385  cardval3ex  7388  carden2bex  7393  genpdflem  7726  genipv  7728  genpelxp  7730  addcomprg  7797  mulcomprg  7799  uzval  9756  ixxval  10130  fzval  10244  hashinfom  11039  hashennn  11041  shftfn  11384  bitsfval  12502  gcdval  12529  lcmval  12634  isprm  12680  odzval  12813  pceulem  12866  pceu  12867  pcval  12868  pczpre  12869  pcdiv  12874  lspval  14403  istopon  14736  toponsspwpwg  14745  clsval  14834  neival  14866  cnpval  14921  blvalps  15111  blval  15112  limccl  15382  ellimc3apf  15383  eldvap  15405  sgmval  15706  vtxdgfifival  16141  clwwlknon  16279  clwwlk0on0  16281