Theorem rabbidv 2675

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 274	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	rabbidva 2674	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1331   e. wcel 1480   {crab 2420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-ral 2421  df-rab 2425

This theorem is referenced by:  rabeqbidv  2681  difeq2  3188  seex  4257  mptiniseg  5033  supeq1  6873  supeq2  6876  supeq3  6877  cardcl  7037  isnumi  7038  cardval3ex  7041  carden2bex  7045  genpdflem  7315  genipv  7317  genpelxp  7319  addcomprg  7386  mulcomprg  7388  uzval  9328  ixxval  9679  fzval  9792  hashinfom  10524  hashennn  10526  shftfn  10596  gcdval  11648  lcmval  11744  isprm  11790  istopon  12180  toponsspwpwg  12189  clsval  12280  neival  12312  cnpval  12367  blvalps  12557  blval  12558  limccl  12797  ellimc3apf  12798  eldvap  12820