Theorem pm14.122c

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

	Ref	Expression
Assertion	pm14.122c	$$⊢A\in V\to \left(\forall x\left(\phi \leftrightarrow x=A\right)\leftrightarrow \left(\forall x\left(\phi \to x=A\right)\wedge \exists x\phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		pm14.122b	$$⊢A\in V\to \left(\left(\forall x\left(\phi \to x=A\right)\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\forall x\left(\phi \to x=A\right)\wedge \exists x\phi \right)\right)$$
3	1 2	bitrd	$$⊢A\in V\to \left(\forall x\left(\phi \leftrightarrow x=A\right)\leftrightarrow \left(\forall x\left(\phi \to x=A\right)\wedge \exists x\phi \right)\right)$$