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

Metamath Proof Explorer

Theorem rabbidva2

Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017)

		Ref	Expression
	Hypothesis	rabbidva2.1	$⊢ φ \to ((x \in A \land ψ) \leftrightarrow (x \in B \land χ))$
	Assertion	rabbidva2	$⊢ φ \to \{x \in A \| ψ\} = \{x \in B \| χ\}$

Step	Hyp	Ref	Expression
1		rabbidva2.1	$⊢ φ \to ((x \in A \land ψ) \leftrightarrow (x \in B \land χ))$
2	1	abbidv	$⊢ φ \to \{x \| (x \in A \land ψ)\} = \{x \| (x \in B \land χ)\}$
3		df-rab	$⊢ \{x \in A \| ψ\} = \{x \| (x \in A \land ψ)\}$
4		df-rab	$⊢ \{x \in B \| χ\} = \{x \| (x \in B \land χ)\}$
5	2 3 4	3eqtr4g	$⊢ φ \to \{x \in A \| ψ\} = \{x \in B \| χ\}$