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\in A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	riotabiia	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x\in A|\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		riotabiia.1	$$⊢x\in A\to \left(\phi \leftrightarrow \psi \right)$$
2		eqid	$$⊢\mathrm{V}=\mathrm{V}$$
3	1	adantl	$$⊢\left(\mathrm{V}=\mathrm{V}\wedge x\in A\right)\to \left(\phi \leftrightarrow \psi \right)$$
4	3	riotabidva	$$⊢\mathrm{V}=\mathrm{V}\to \left(\iota x\in A|\phi \right)=\left(\iota x\in A|\psi \right)$$
5	2 4	ax-mp	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x\in A|\psi \right)$$