Theorem iotasbcq

Description: Theorem *14.272 in WhiteheadRussell p. 193. (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	iotasbcq	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/y\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\psi \right)/y\underset{\dot{}}{]}\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		iotabi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\iota x|\phi \right)=\left(\iota x|\psi \right)$$
2	1	sbceq1d	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/y\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\psi \right)/y\underset{\dot{}}{]}\chi \right)$$