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	$⊢ Ⅎ x φ$
	rabbida.1	$⊢ (φ \land x \in A) \to (ψ \leftrightarrow χ)$
Assertion	rabbida	$⊢ φ \to \{x \in A \| ψ\} = \{x \in A \| χ\}$

Proof

Step	Hyp	Ref	Expression
1		rabbida.n	$⊢ Ⅎ x φ$
2		rabbida.1	$⊢ (φ \land x \in A) \to (ψ \leftrightarrow χ)$
3	2	pm5.32da	$⊢ φ \to ((x \in A \land ψ) \leftrightarrow (x \in A \land χ))$
4	1 3	rabbida4	$⊢ φ \to \{x \in A \| ψ\} = \{x \in A \| χ\}$