Theorem fveqsb

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

	Ref	Expression
Hypotheses	fveqsb.2	$$⊢x=F\left(A\right)\to \left(\phi \leftrightarrow \psi \right)$$
	fveqsb.3	$$⊢Ⅎx\psi$$
Assertion	fveqsb	$$⊢\exists !yAFy\to \left(\psi \leftrightarrow \exists x\left(\forall y\left(AFy\leftrightarrow y=x\right)\wedge \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveqsb.2	$$⊢x=F\left(A\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		fveqsb.3	$$⊢Ⅎx\psi$$
3		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
4	2 1	sbciegf	$$⊢F\left(A\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}F\left(A\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
5	3 4	ax-mp	$$⊢\underset{\dot{}}{[}F\left(A\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
6		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)$$
7	5 6	bitr3id	$$⊢\exists !yAFy\to \left(\psi \leftrightarrow \exists x\left(\forall y\left(AFy\leftrightarrow y=x\right)\wedge \phi \right)\right)$$