Theorem rabbidv 2609

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1290   e. wcel 1439   {crab 2364

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-ral 2365  df-rab 2369

This theorem is referenced by:  rabeqbidv  2615  difeq2  3113  seex  4171  mptiniseg  4938  supeq1  6735  supeq2  6738  supeq3  6739  cardcl  6870  isnumi  6871  cardval3ex  6874  carden2bex  6878  genpdflem  7127  genipv  7129  genpelxp  7131  addcomprg  7198  mulcomprg  7200  uzval  9082  ixxval  9375  fzval  9487  hashinfom  10247  hashennn  10249  shftfn  10319  gcdval  11290  lcmval  11384  isprm  11430  istopon  11773  toponsspwpwg  11781  clsval  11872