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	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( [ ( 𝐹 ‘ 𝐴 ) / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-fv	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 )
2		dfsbcq	⊢ ( ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 ) → ( [ ( 𝐹 ‘ 𝐴 ) / 𝑥 ] 𝜑 ↔ [ ( ℩ 𝑦 𝐴 𝐹 𝑦 ) / 𝑥 ] 𝜑 ) )
3	1 2	ax-mp	⊢ ( [ ( 𝐹 ‘ 𝐴 ) / 𝑥 ] 𝜑 ↔ [ ( ℩ 𝑦 𝐴 𝐹 𝑦 ) / 𝑥 ] 𝜑 )
4		iotasbc	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( [ ( ℩ 𝑦 𝐴 𝐹 𝑦 ) / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) ∧ 𝜑 ) ) )
5	3 4	syl5bb	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( [ ( 𝐹 ‘ 𝐴 ) / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) ∧ 𝜑 ) ) )