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	⊢ ( 𝑥 = ( 𝐹 ‘ 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )
	fveqsb.3	⊢ Ⅎ 𝑥 𝜓
Assertion	fveqsb	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( 𝜓 ↔ ∃ 𝑥 ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveqsb.2	⊢ ( 𝑥 = ( 𝐹 ‘ 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )
2		fveqsb.3	⊢ Ⅎ 𝑥 𝜓
3		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
4	2 1	sbciegf	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ V → ( [ ( 𝐹 ‘ 𝐴 ) / 𝑥 ] 𝜑 ↔ 𝜓 ) )
5	3 4	ax-mp	⊢ ( [ ( 𝐹 ‘ 𝐴 ) / 𝑥 ] 𝜑 ↔ 𝜓 )
6		fvsb	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( [ ( 𝐹 ‘ 𝐴 ) / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) ∧ 𝜑 ) ) )
7	5 6	bitr3id	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( 𝜓 ↔ ∃ 𝑥 ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) ∧ 𝜑 ) ) )