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  9939  ixxval  10315  fzval  10430  hashinfom  11239  hashennn  11241  ssenneg  11302  hashfibclem  11304  hashfibc  11305  shftfn  11611  bitsfval  12734  gcdval  12761  lcmval  12866  isprm  12912  odzval  13049  pceulem  13102  pceu  13103  pcval  13104  pczpre  13105  pcdiv  13110  ballotfilemi  13301  ballotfi  13340  cntzval  14153  cntzsnval  14156  lspval  14836  aspval  15124  psrass1filem  15177  psrmulvalfi  15188  istopon  15239  toponsspwpwg  15248  clsval  15337  neival  15369  cnpval  15424  blvalps  15614  blval  15615  limccl  15885  ellimc3apf  15886  eldvap  15908  sgmval  16252  vtxdgfifival  16737  clwwlknon  16875  clwwlk0on0  16877  eupth2fi  16925