Theorem rabbidv 2762

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   e. wcel 2177   {crab 2489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-ral 2490  df-rab 2494

This theorem is referenced by:  rabeqbidv  2768  difeq2  3289  seex  4390  mptiniseg  5186  elovmporab  6159  supeq1  7103  supeq2  7106  supeq3  7107  cardcl  7303  isnumi  7304  cardval3ex  7307  carden2bex  7312  genpdflem  7640  genipv  7642  genpelxp  7644  addcomprg  7711  mulcomprg  7713  uzval  9670  ixxval  10038  fzval  10152  hashinfom  10945  hashennn  10947  shftfn  11210  bitsfval  12328  gcdval  12355  lcmval  12460  isprm  12506  odzval  12639  pceulem  12692  pceu  12693  pcval  12694  pczpre  12695  pcdiv  12700  lspval  14227  istopon  14560  toponsspwpwg  14569  clsval  14658  neival  14690  cnpval  14745  blvalps  14935  blval  14936  limccl  15206  ellimc3apf  15207  eldvap  15229  sgmval  15530