Theorem pm13.195

Description: Theorem *13.195 in WhiteheadRussell p. 179. This theorem is very similar to sbc5 . (Contributed by Andrew Salmon, 3-Jun-2011) (Revised by NM, 4-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		sbc5	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\phi \leftrightarrow \exists y\left(y=A\wedge \phi \right)$$
2	1	bicomi	$$⊢\exists y\left(y=A\wedge \phi \right)\leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}\phi$$