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	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
Assertion	riotabidva	|- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. A ch ) )

Proof

Step	Hyp	Ref	Expression
1		riotabidva.1	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
2	1	pm5.32da	|- ( 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 ) )