Theorem rabbia2

Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		rabbia2.1	|- ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) )
2	1	a1i	|- ( T. -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )
3	2	rabbidva2	|- ( T. -> { x e. A | ps } = { x e. B | ch } )
4	3	mptru	|- { x e. A | ps } = { x e. B | ch }