Theorem rabbidv 2728

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   e. wcel 2148   {crab 2459

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-ral 2460  df-rab 2464

This theorem is referenced by:  rabeqbidv  2734  difeq2  3249  seex  4337  mptiniseg  5125  supeq1  6988  supeq2  6991  supeq3  6992  cardcl  7183  isnumi  7184  cardval3ex  7187  carden2bex  7191  genpdflem  7509  genipv  7511  genpelxp  7513  addcomprg  7580  mulcomprg  7582  uzval  9533  ixxval  9899  fzval  10013  hashinfom  10761  hashennn  10763  shftfn  10836  gcdval  11963  lcmval  12066  isprm  12112  odzval  12244  pceulem  12297  pceu  12298  pcval  12299  pczpre  12300  pcdiv  12305  lspval  13483  istopon  13653  toponsspwpwg  13662  clsval  13751  neival  13783  cnpval  13838  blvalps  14028  blval  14029  limccl  14268  ellimc3apf  14269  eldvap  14291