Theorem rabbidva

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

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

Proof

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