Theorem pm14.122a

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

	Ref	Expression
Assertion	pm14.122a	$$⊢A\in V\to \left(\forall x\left(\phi \leftrightarrow x=A\right)\leftrightarrow \left(\forall x\left(\phi \to x=A\right)\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		albiim	$$⊢\forall x\left(\phi \leftrightarrow x=A\right)\leftrightarrow \left(\forall x\left(\phi \to x=A\right)\wedge \forall x\left(x=A\to \phi \right)\right)$$
2		sbc6g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$
3	2	bicomd	$$⊢A\in V\to \left(\forall x\left(x=A\to \phi \right)\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4	3	anbi2d	$$⊢A\in V\to \left(\left(\forall x\left(\phi \to x=A\right)\wedge \forall x\left(x=A\to \phi \right)\right)\leftrightarrow \left(\forall x\left(\phi \to x=A\right)\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
5	1 4	syl5bb	$$⊢A\in V\to \left(\forall x\left(\phi \leftrightarrow x=A\right)\leftrightarrow \left(\forall x\left(\phi \to x=A\right)\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$