Theorem pm14.123c

Description: Theorem *14.123 in WhiteheadRussell p. 185. (Contributed by Andrew Salmon, 9-Jun-2011)

	Ref	Expression
Assertion	pm14.123c	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\forall z\forall w\left(\phi \leftrightarrow \left(z=A\wedge w=B\right)\right)\leftrightarrow \left(\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\wedge \exists z\exists w\phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pm14.123a	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\forall z\forall w\left(\phi \leftrightarrow \left(z=A\wedge w=B\right)\right)\leftrightarrow \left(\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\wedge \underset{\dot{}}{[}A/z\underset{\dot{}}{]}\underset{\dot{}}{[}B/w\underset{\dot{}}{]}\phi \right)\right)$$
2		pm14.123b	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left(\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\wedge \underset{\dot{}}{[}A/z\underset{\dot{}}{]}\underset{\dot{}}{[}B/w\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\wedge \exists z\exists w\phi \right)\right)$$
3	1 2	bitrd	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\forall z\forall w\left(\phi \leftrightarrow \left(z=A\wedge w=B\right)\right)\leftrightarrow \left(\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\wedge \exists z\exists w\phi \right)\right)$$