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 ` A ) -> ( ph <-> ps ) )
	fveqsb.3	|- F/ x ps
Assertion	fveqsb	|- ( E! y A F y -> ( ps <-> E. x ( A. y ( A F y <-> y = x ) /\ ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveqsb.2	|- ( x = ( F ` A ) -> ( ph <-> ps ) )
2		fveqsb.3	|- F/ x ps
3		fvex	|- ( F ` A ) e. _V
4	2 1	sbciegf	|- ( ( F ` A ) e. _V -> ( [. ( F ` A ) / x ]. ph <-> ps ) )
5	3 4	ax-mp	|- ( [. ( F ` A ) / x ]. ph <-> ps )
6		fvsb	|- ( E! y A F y -> ( [. ( F ` A ) / x ]. ph <-> E. x ( A. y ( A F y <-> y = x ) /\ ph ) ) )
7	5 6	bitr3id	|- ( E! y A F y -> ( ps <-> E. x ( A. y ( A F y <-> y = x ) /\ ph ) ) )