This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rabbida

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). Version of rabbidva with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 14-Mar-2025)

	Ref	Expression
Hypotheses	rabbida.n	\|- F/ x ph
	rabbida.1	\|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
Assertion	rabbida	\|- ( ph -> { x e. A \| ps } = { x e. A \| ch } )

Proof

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