Theorem iotabii

Description: Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypothesis	iotabii.1	$$⊢\phi \leftrightarrow \psi$$
Assertion	iotabii	$$⊢\left(\iota x|\phi \right)=\left(\iota x|\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		iotabii.1	$$⊢\phi \leftrightarrow \psi$$
2		iotabi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\iota x|\phi \right)=\left(\iota x|\psi \right)$$
3	2 1	mpg	$$⊢\left(\iota x|\phi \right)=\left(\iota x|\psi \right)$$