Theorem rabbidv 2810

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209   {crab 2532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-ral 2533  df-rab 2537

This theorem is used by:  rabeqbidv  2816  difeq2  3341  seex  4482  mptiniseg  5285  elovmporab  6292  supeq1  7332  supeq2  7335  supeq3  7336  cardcl  7532  isnumi  7533  cardval3ex  7536  carden2bex  7541  genpdflem  7880  genipv  7882  genpelxp  7884  addcomprg  7951  mulcomprg  7953  uzval  9938  ixxval  10314  fzval  10429  hashinfom  11238  hashennn  11240  ssenneg  11301  hashfibclem  11303  hashfibc  11304  shftfn  11610  bitsfval  12733  gcdval  12760  lcmval  12865  isprm  12911  odzval  13048  pceulem  13101  pceu  13102  pcval  13103  pczpre  13104  pcdiv  13109  ballotfilemi  13300  ballotfi  13339  cntzval  14152  cntzsnval  14155  lspval  14835  aspval  15123  psrass1filem  15186  psrmulvalfi  15197  istopon  15256  toponsspwpwg  15265  clsval  15354  neival  15386  cnpval  15441  blvalps  15631  blval  15632  limccl  15902  ellimc3apf  15903  eldvap  15925  sgmval  16269  vtxdgfifival  16754  clwwlknon  16892  clwwlk0on0  16894  eupth2fi  16942