Theorem fvsb

Description: Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011)

	Ref	Expression
Assertion	fvsb	$$⊢\exists !yAFy\to \left(\underset{\dot{}}{[}F\left(A\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \exists x\left(\forall y\left(AFy\leftrightarrow y=x\right)\wedge \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-fv	$$⊢F\left(A\right)=\left(\iota y|AFy\right)$$
2		dfsbcq	$$⊢F\left(A\right)=\left(\iota y|AFy\right)\to \left(\underset{\dot{}}{[}F\left(A\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(\iota y|AFy\right)/x\underset{\dot{}}{]}\phi \right)$$
3	1 2	ax-mp	$$⊢\underset{\dot{}}{[}F\left(A\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(\iota y|AFy\right)/x\underset{\dot{}}{]}\phi$$
4		iotasbc	$$⊢\exists !yAFy\to \left(\underset{\dot{}}{[}\left(\iota y|AFy\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \exists x\left(\forall y\left(AFy\leftrightarrow y=x\right)\wedge \phi \right)\right)$$
5	3 4	bitrid	$$⊢\exists !yAFy\to \left(\underset{\dot{}}{[}F\left(A\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \exists x\left(\forall y\left(AFy\leftrightarrow y=x\right)\wedge \phi \right)\right)$$