Theorem rabbidv 2714

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 2713	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1343   e. wcel 2136   {crab 2447

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-ral 2448  df-rab 2452

This theorem is referenced by:  rabeqbidv  2720  difeq2  3233  seex  4312  mptiniseg  5097  supeq1  6947  supeq2  6950  supeq3  6951  cardcl  7133  isnumi  7134  cardval3ex  7137  carden2bex  7141  genpdflem  7444  genipv  7446  genpelxp  7448  addcomprg  7515  mulcomprg  7517  uzval  9464  ixxval  9828  fzval  9942  hashinfom  10687  hashennn  10689  shftfn  10762  gcdval  11888  lcmval  11991  isprm  12037  odzval  12169  pceulem  12222  pceu  12223  pcval  12224  pczpre  12225  pcdiv  12230  istopon  12611  toponsspwpwg  12620  clsval  12711  neival  12743  cnpval  12798  blvalps  12988  blval  12989  limccl  13228  ellimc3apf  13229  eldvap  13251