Metamath Proof Explorer

Theorem riotabidva

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). ( rabbidva analog.) (Contributed by NM, 17-Jan-2012)

		Ref	Expression
	Hypothesis	riotabidva.1	$⊢ (φ \land x \in A) \to (ψ \leftrightarrow χ)$
	Assertion	riotabidva	$⊢ φ \to (ι x \in A \| ψ) = (ι x \in A \| χ)$

Step	Hyp	Ref	Expression
1		riotabidva.1	$⊢ (φ \land x \in A) \to (ψ \leftrightarrow χ)$
2	1	pm5.32da	$⊢ φ \to ((x \in A \land ψ) \leftrightarrow (x \in A \land χ))$
3	2	iotabidv	$⊢ φ \to (ι x \| (x \in A \land ψ)) = (ι x \| (x \in A \land χ))$
4		df-riota	$⊢ (ι x \in A \| ψ) = (ι x \| (x \in A \land ψ))$
5		df-riota	$⊢ (ι x \in A \| χ) = (ι x \| (x \in A \land χ))$
6	3 4 5	3eqtr4g	$⊢ φ \to (ι x \in A \| ψ) = (ι x \in A \| χ)$