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  6987  supeq2  6990  supeq3  6991  cardcl  7182  isnumi  7183  cardval3ex  7186  carden2bex  7190  genpdflem  7508  genipv  7510  genpelxp  7512  addcomprg  7579  mulcomprg  7581  uzval  9532  ixxval  9898  fzval  10012  hashinfom  10760  hashennn  10762  shftfn  10835  gcdval  11962  lcmval  12065  isprm  12111  odzval  12243  pceulem  12296  pceu  12297  pcval  12298  pczpre  12299  pcdiv  12304  lspval  13482  istopon  13598  toponsspwpwg  13607  clsval  13696  neival  13728  cnpval  13783  blvalps  13973  blval  13974  limccl  14213  ellimc3apf  14214  eldvap  14236