Theorem pm14.123a

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

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

Proof

Step	Hyp	Ref	Expression
1		2albiim	$$⊢\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 \forall z\forall w\left(\left(z=A\wedge w=B\right)\to \phi \right)\right)$$
2		2sbc6g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\forall z\forall w\left(\left(z=A\wedge w=B\right)\to \phi \right)\leftrightarrow \underset{\dot{}}{[}A/z\underset{\dot{}}{]}\underset{\dot{}}{[}B/w\underset{\dot{}}{]}\phi \right)$$
3	2	anbi2d	$$⊢\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 \forall z\forall w\left(\left(z=A\wedge w=B\right)\to \phi \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)$$
4	1 3	syl5bb	$$⊢\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)$$