Theorem cdlemk40f

Description: TODO: fix comment. (Contributed by NM, 31-Jul-2013)

	Ref	Expression
Hypotheses	cdlemk40.x	⊢ 𝑋 = ( ℩ 𝑧 ∈ 𝑇 𝜑 )
	cdlemk40.u	⊢ 𝑈 = ( 𝑔 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
Assertion	cdlemk40f	⊢ ( ( 𝐹 ≠ 𝑁 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑈 ‘ 𝐺 ) = ⦋ 𝐺 / 𝑔 ⦌ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		cdlemk40.x	⊢ 𝑋 = ( ℩ 𝑧 ∈ 𝑇 𝜑 )
2		cdlemk40.u	⊢ 𝑈 = ( 𝑔 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
3	1 2	cdlemk40	⊢ ( 𝐺 ∈ 𝑇 → ( 𝑈 ‘ 𝐺 ) = if ( 𝐹 = 𝑁 , 𝐺 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) )
4		ifnefalse	⊢ ( 𝐹 ≠ 𝑁 → if ( 𝐹 = 𝑁 , 𝐺 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) = ⦋ 𝐺 / 𝑔 ⦌ 𝑋 )
5	3 4	sylan9eqr	⊢ ( ( 𝐹 ≠ 𝑁 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑈 ‘ 𝐺 ) = ⦋ 𝐺 / 𝑔 ⦌ 𝑋 )