Theorem pm13.192

Description: Theorem *13.192 in WhiteheadRussell p. 179. (Contributed by Andrew Salmon, 3-Jun-2011) (Revised by NM, 4-Jan-2017)

	Ref	Expression
Assertion	pm13.192	$$⊢\exists y\left(\forall x\left(x=A\leftrightarrow x=y\right)\wedge \phi \right)\leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		biimpr	$$⊢\left(x=A\leftrightarrow x=y\right)\to \left(x=y\to x=A\right)$$
2	1	alimi	$$⊢\forall x\left(x=A\leftrightarrow x=y\right)\to \forall x\left(x=y\to x=A\right)$$
3		eqeq1	$$⊢x=y\to \left(x=A\leftrightarrow y=A\right)$$
4	3	equsalvw	$$⊢\forall x\left(x=y\to x=A\right)\leftrightarrow y=A$$
5	2 4	sylib	$$⊢\forall x\left(x=A\leftrightarrow x=y\right)\to y=A$$
6		eqeq2	$$⊢A=y\to \left(x=A\leftrightarrow x=y\right)$$
7	6	eqcoms	$$⊢y=A\to \left(x=A\leftrightarrow x=y\right)$$
8	7	alrimiv	$$⊢y=A\to \forall x\left(x=A\leftrightarrow x=y\right)$$
9	5 8	impbii	$$⊢\forall x\left(x=A\leftrightarrow x=y\right)\leftrightarrow y=A$$
10	9	anbi1i	$$⊢\left(\forall x\left(x=A\leftrightarrow x=y\right)\wedge \phi \right)\leftrightarrow \left(y=A\wedge \phi \right)$$
11	10	exbii	$$⊢\exists y\left(\forall x\left(x=A\leftrightarrow x=y\right)\wedge \phi \right)\leftrightarrow \exists y\left(y=A\wedge \phi \right)$$
12		sbc5	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\phi \leftrightarrow \exists y\left(y=A\wedge \phi \right)$$
13	11 12	bitr4i	$$⊢\exists y\left(\forall x\left(x=A\leftrightarrow x=y\right)\wedge \phi \right)\leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}\phi$$