Theorem rabbidv 2752

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   e. wcel 2167   {crab 2479

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-ral 2480  df-rab 2484

This theorem is referenced by:  rabeqbidv  2758  difeq2  3275  seex  4370  mptiniseg  5164  elovmporab  6123  supeq1  7052  supeq2  7055  supeq3  7056  cardcl  7248  isnumi  7249  cardval3ex  7252  carden2bex  7256  genpdflem  7574  genipv  7576  genpelxp  7578  addcomprg  7645  mulcomprg  7647  uzval  9603  ixxval  9971  fzval  10085  hashinfom  10870  hashennn  10872  shftfn  10989  bitsfval  12107  gcdval  12126  lcmval  12231  isprm  12277  odzval  12410  pceulem  12463  pceu  12464  pcval  12465  pczpre  12466  pcdiv  12471  lspval  13946  istopon  14249  toponsspwpwg  14258  clsval  14347  neival  14379  cnpval  14434  blvalps  14624  blval  14625  limccl  14895  ellimc3apf  14896  eldvap  14918  sgmval  15219