Theorem rabbidv 2788

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 2787	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  2794  difeq2  3316  seex  4426  mptiniseg  5223  elovmporab  6205  supeq1  7153  supeq2  7156  supeq3  7157  cardcl  7353  isnumi  7354  cardval3ex  7357  carden2bex  7362  genpdflem  7694  genipv  7696  genpelxp  7698  addcomprg  7765  mulcomprg  7767  uzval  9724  ixxval  10092  fzval  10206  hashinfom  11000  hashennn  11002  shftfn  11335  bitsfval  12453  gcdval  12480  lcmval  12585  isprm  12631  odzval  12764  pceulem  12817  pceu  12818  pcval  12819  pczpre  12820  pcdiv  12825  lspval  14354  istopon  14687  toponsspwpwg  14696  clsval  14785  neival  14817  cnpval  14872  blvalps  15062  blval  15063  limccl  15333  ellimc3apf  15334  eldvap  15356  sgmval  15657