Theorem iotasbc2

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

	Ref	Expression
Assertion	iotasbc2	$$⊢\left(\exists !x\phi \wedge \exists !x\psi \right)\to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left(\iota x|\psi \right)/z\underset{\dot{}}{]}\chi \leftrightarrow \exists y\exists z\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		iotasbc	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left(\iota x|\psi \right)/z\underset{\dot{}}{]}\chi \leftrightarrow \exists y\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \underset{\dot{}}{[}\left(\iota x|\psi \right)/z\underset{\dot{}}{]}\chi \right)\right)$$
2		iotasbc	$$⊢\exists !x\psi \to \left(\underset{\dot{}}{[}\left(\iota x|\psi \right)/z\underset{\dot{}}{]}\chi \leftrightarrow \exists z\left(\forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)$$
3	2	anbi2d	$$⊢\exists !x\psi \to \left(\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \underset{\dot{}}{[}\left(\iota x|\psi \right)/z\underset{\dot{}}{]}\chi \right)\leftrightarrow \left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \exists z\left(\forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)\right)$$
4		3anass	$$⊢\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\leftrightarrow \left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \left(\forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)$$
5	4	exbii	$$⊢\exists z\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\leftrightarrow \exists z\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \left(\forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)$$
6		19.42v	$$⊢\exists z\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \left(\forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)\leftrightarrow \left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \exists z\left(\forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)$$
7	5 6	bitr2i	$$⊢\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \exists z\left(\forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)\leftrightarrow \exists z\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)$$
8	3 7	bitrdi	$$⊢\exists !x\psi \to \left(\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \underset{\dot{}}{[}\left(\iota x|\psi \right)/z\underset{\dot{}}{]}\chi \right)\leftrightarrow \exists z\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)$$
9	8	exbidv	$$⊢\exists !x\psi \to \left(\exists y\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \underset{\dot{}}{[}\left(\iota x|\psi \right)/z\underset{\dot{}}{]}\chi \right)\leftrightarrow \exists y\exists z\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)$$
10	1 9	sylan9bb	$$⊢\left(\exists !x\phi \wedge \exists !x\psi \right)\to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}\left(\iota x|\psi \right)/z\underset{\dot{}}{]}\chi \leftrightarrow \exists y\exists z\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \forall x\left(\psi \leftrightarrow x=z\right)\wedge \chi \right)\right)$$