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

Metamath Proof Explorer

Theorem rabbidaOLD

Description: Obsolete version of rabbida as of 14-Mar-2025. (Contributed by BJ, 27-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rabbidaOLD.n	$⊢ Ⅎ x φ$
	rabbidaOLD.1	$⊢ (φ \land x \in A) \to (ψ \leftrightarrow χ)$
Assertion	rabbidaOLD	$⊢ φ \to \{x \in A \| ψ\} = \{x \in A \| χ\}$

Proof

Step	Hyp	Ref	Expression
1		rabbidaOLD.n	$⊢ Ⅎ x φ$
2		rabbidaOLD.1	$⊢ (φ \land x \in A) \to (ψ \leftrightarrow χ)$
3	2	ex	$⊢ φ \to (x \in A \to (ψ \leftrightarrow χ))$
4	1 3	ralrimi	$⊢ φ \to \forall x \in A (ψ \leftrightarrow χ)$
5		rabbi	$⊢ \forall x \in A (ψ \leftrightarrow χ) \leftrightarrow \{x \in A \| ψ\} = \{x \in A \| χ\}$
6	4 5	sylib	$⊢ φ \to \{x \in A \| ψ\} = \{x \in A \| χ\}$