Theorem riotabiia

Description: Equivalent wff's yield equal restricted iotas (inference form). ( rabbiia analog.) (Contributed by NM, 16-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		riotabiia.1	|- ( x e. A -> ( ph <-> ps ) )
2		eqid	|- _V = _V
3	1	adantl	|- ( ( _V = _V /\ x e. A ) -> ( ph <-> ps ) )
4	3	riotabidva	|- ( _V = _V -> ( iota_ x e. A ph ) = ( iota_ x e. A ps ) )
5	2 4	ax-mp	|- ( iota_ x e. A ph ) = ( iota_ x e. A ps )