Theorem riotabidv

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

	Ref	Expression
Hypothesis	riotabidv.1	|- ( ph -> ( ps <-> ch ) )
Assertion	riotabidv	|- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. A ch ) )

Proof

Step	Hyp	Ref	Expression
1		riotabidv.1	|- ( ph -> ( ps <-> ch ) )
2	1	anbi2d	|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. A /\ ch ) ) )
3	2	iotabidv	|- ( ph -> ( iota x ( x e. A /\ ps ) ) = ( iota x ( x e. A /\ ch ) ) )
4		df-riota	|- ( iota_ x e. A ps ) = ( iota x ( x e. A /\ ps ) )
5		df-riota	|- ( iota_ x e. A ch ) = ( iota x ( x e. A /\ ch ) )
6	3 4 5	3eqtr4g	|- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. A ch ) )