Theorem rabbidva 2760

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.)

Hypothesis

Ref	Expression
rabbidva.1	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )

Assertion

Ref	Expression
rabbidva	|- ( 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 rabbidva

Step	Hyp	Ref	Expression
1		rabbidva.1	. . 3 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
2	1	ralrimiva 2579	. 2 |- ( ph -> A. x e. A ( ps <-> ch ) )
3		rabbi 2684	. 2 |- ( A. x e. A ( ps <-> ch ) <-> { x e. A | ps } = { x e. A | ch } )
4	2, 3	sylib 122	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1373   e. wcel 2176   A.wral 2484   {crab 2488

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-ral 2489  df-rab 2493

This theorem is referenced by:  rabbidv  2761  rabeqbidva  2768  rabbi2dva  3381  rabxfrd  4517  onsucmin  4556  seinxp  4747  fniniseg2  5704  fnniniseg2  5705  f1oresrab  5747  dfinfre  9031  minmax  11574  xrminmax  11609  iooinsup  11621  gcdass  12369  lcmass  12440  pcneg  12681  bdbl  15008  xmetxpbl  15013  lgsquadlem1  15587  lgsquadlem2  15588  2lgslem1a  15598  2omap  15969