Theorem riotaeqdv

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

	Ref	Expression
Hypothesis	riotaeqdv.1	|- ( ph -> A = B )
Assertion	riotaeqdv	|- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		riotaeqdv.1	|- ( ph -> A = B )
2	1	eleq2d	|- ( ph -> ( x e. A <-> x e. B ) )
3	2	anbi1d	|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ps ) ) )
4	3	iotabidv	|- ( ph -> ( iota x ( x e. A /\ ps ) ) = ( iota x ( x e. B /\ ps ) ) )
5		df-riota	|- ( iota_ x e. A ps ) = ( iota x ( x e. A /\ ps ) )
6		df-riota	|- ( iota_ x e. B ps ) = ( iota x ( x e. B /\ ps ) )
7	4 5 6	3eqtr4g	|- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. B ps ) )