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	|- ( E! y A F y -> ( [. ( F ` A ) / x ]. ph <-> E. x ( A. y ( A F y <-> y = x ) /\ ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-fv	|- ( F ` A ) = ( iota y A F y )
2		dfsbcq	|- ( ( F ` A ) = ( iota y A F y ) -> ( [. ( F ` A ) / x ]. ph <-> [. ( iota y A F y ) / x ]. ph ) )
3	1 2	ax-mp	|- ( [. ( F ` A ) / x ]. ph <-> [. ( iota y A F y ) / x ]. ph )
4		iotasbc	|- ( E! y A F y -> ( [. ( iota y A F y ) / x ]. ph <-> E. x ( A. y ( A F y <-> y = x ) /\ ph ) ) )
5	3 4	bitrid	|- ( E! y A F y -> ( [. ( F ` A ) / x ]. ph <-> E. x ( A. y ( A F y <-> y = x ) /\ ph ) ) )