Theorem rabbidv 2670

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

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

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 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-ral 2419  df-rab 2423

This theorem is referenced by:  rabeqbidv  2676  difeq2  3183  seex  4252  mptiniseg  5028  supeq1  6866  supeq2  6869  supeq3  6870  cardcl  7030  isnumi  7031  cardval3ex  7034  carden2bex  7038  genpdflem  7308  genipv  7310  genpelxp  7312  addcomprg  7379  mulcomprg  7381  uzval  9321  ixxval  9672  fzval  9785  hashinfom  10517  hashennn  10519  shftfn  10589  gcdval  11637  lcmval  11733  isprm  11779  istopon  12169  toponsspwpwg  12178  clsval  12269  neival  12301  cnpval  12356  blvalps  12546  blval  12547  limccl  12786  ellimc3apf  12787  eldvap  12809