Theorem rabbidv 2719

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   e. wcel 2141   {crab 2452

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-ral 2453  df-rab 2457

This theorem is referenced by:  rabeqbidv  2725  difeq2  3239  seex  4320  mptiniseg  5105  supeq1  6963  supeq2  6966  supeq3  6967  cardcl  7158  isnumi  7159  cardval3ex  7162  carden2bex  7166  genpdflem  7469  genipv  7471  genpelxp  7473  addcomprg  7540  mulcomprg  7542  uzval  9489  ixxval  9853  fzval  9967  hashinfom  10712  hashennn  10714  shftfn  10788  gcdval  11914  lcmval  12017  isprm  12063  odzval  12195  pceulem  12248  pceu  12249  pcval  12250  pczpre  12251  pcdiv  12256  istopon  12805  toponsspwpwg  12814  clsval  12905  neival  12937  cnpval  12992  blvalps  13182  blval  13183  limccl  13422  ellimc3apf  13423  eldvap  13445