riotaeqdv

Description: Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011)

		Ref	Expression
	Hypothesis	riotaeqdv.1	$⊢ φ \to A = B$
	Assertion	riotaeqdv	$⊢ φ \to (ι x \in A \| ψ) = (ι x \in B \| ψ)$

Step	Hyp	Ref	Expression
1		riotaeqdv.1	$⊢ φ \to A = B$
2	1	eleq2d	$⊢ φ \to (x \in A \leftrightarrow x \in B)$
3	2	anbi1d	$⊢ φ \to ((x \in A \land ψ) \leftrightarrow (x \in B \land ψ))$
4	3	iotabidv	$⊢ φ \to (ι x \| (x \in A \land ψ)) = (ι x \| (x \in B \land ψ))$
5		df-riota	$⊢ (ι x \in A \| ψ) = (ι x \| (x \in A \land ψ))$
6		df-riota	$⊢ (ι x \in B \| ψ) = (ι x \| (x \in B \land ψ))$
7	4 5 6	3eqtr4g	$⊢ φ \to (ι x \in A \| ψ) = (ι x \in B \| ψ)$

Metamath Proof Explorer