Theorem rabbidv 2789

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395   e. wcel 2200   {crab 2512

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-ral 2513  df-rab 2517

This theorem is referenced by:  rabeqbidv  2795  difeq2  3317  seex  4430  mptiniseg  5229  elovmporab  6217  supeq1  7176  supeq2  7179  supeq3  7180  cardcl  7376  isnumi  7377  cardval3ex  7380  carden2bex  7385  genpdflem  7717  genipv  7719  genpelxp  7721  addcomprg  7788  mulcomprg  7790  uzval  9747  ixxval  10121  fzval  10235  hashinfom  11030  hashennn  11032  shftfn  11375  bitsfval  12493  gcdval  12520  lcmval  12625  isprm  12671  odzval  12804  pceulem  12857  pceu  12858  pcval  12859  pczpre  12860  pcdiv  12865  lspval  14394  istopon  14727  toponsspwpwg  14736  clsval  14825  neival  14857  cnpval  14912  blvalps  15102  blval  15103  limccl  15373  ellimc3apf  15374  eldvap  15396  sgmval  15697  vtxdgfifival  16097  clwwlknon  16224  clwwlk0on0  16226