Theorem rabbidv

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995)

	Ref	Expression
Hypothesis	rabbidv.1	|- ( ph -> ( ps <-> ch ) )
Assertion	rabbidv	|- ( ph -> { x e. A | ps } = { x e. A | ch } )

Proof

Step	Hyp	Ref	Expression
1		rabbidv.1	|- ( ph -> ( ps <-> ch ) )
2	1	adantr	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	rabbidva	|- ( ph -> { x e. A | ps } = { x e. A | ch } )