Theorem pm14.123b

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

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		2sbc5g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\exists z\exists w\left(\left(z=A\wedge w=B\right)\wedge \phi \right)\leftrightarrow \underset{\dot{}}{[}A/z\underset{\dot{}}{]}\underset{\dot{}}{[}B/w\underset{\dot{}}{]}\phi \right)$$
2	1	adantr	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\right)\to \left(\exists z\exists w\left(\left(z=A\wedge w=B\right)\wedge \phi \right)\leftrightarrow \underset{\dot{}}{[}A/z\underset{\dot{}}{]}\underset{\dot{}}{[}B/w\underset{\dot{}}{]}\phi \right)$$
3		nfa1	$$⊢Ⅎz\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)$$
4		nfa2	$$⊢Ⅎw\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)$$
5		simpr	$$⊢\left(\left(z=A\wedge w=B\right)\wedge \phi \right)\to \phi$$
6		2sp	$$⊢\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\to \left(\phi \to \left(z=A\wedge w=B\right)\right)$$
7	6	ancrd	$$⊢\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\to \left(\phi \to \left(\left(z=A\wedge w=B\right)\wedge \phi \right)\right)$$
8	5 7	impbid2	$$⊢\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\to \left(\left(\left(z=A\wedge w=B\right)\wedge \phi \right)\leftrightarrow \phi \right)$$
9	4 8	exbid	$$⊢\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\to \left(\exists w\left(\left(z=A\wedge w=B\right)\wedge \phi \right)\leftrightarrow \exists w\phi \right)$$
10	3 9	exbid	$$⊢\forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\to \left(\exists z\exists w\left(\left(z=A\wedge w=B\right)\wedge \phi \right)\leftrightarrow \exists z\exists w\phi \right)$$
11	10	adantl	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\right)\to \left(\exists z\exists w\left(\left(z=A\wedge w=B\right)\wedge \phi \right)\leftrightarrow \exists z\exists w\phi \right)$$
12	2 11	bitr3d	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \forall z\forall w\left(\phi \to \left(z=A\wedge w=B\right)\right)\right)\to \left(\underset{\dot{}}{[}A/z\underset{\dot{}}{]}\underset{\dot{}}{[}B/w\underset{\dot{}}{]}\phi \leftrightarrow \exists z\exists w\phi \right)$$
13	12	pm5.32da	$$⊢\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)$$