Theorem ifmpt2v

Description: Move a conditional inside and outside a function in maps-to notation. (Contributed by SN, 16-Oct-2025)

	Ref	Expression
Assertion	ifmpt2v	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝜑 , 𝐵 , 𝐶 ) ) = if ( 𝜑 , ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐵 , 𝐶 ) = 𝐵 )
2	1	mpteq2dv	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝜑 , 𝐵 , 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
3		iftrue	⊢ ( 𝜑 → if ( 𝜑 , ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
4	2 3	eqtr4d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝜑 , 𝐵 , 𝐶 ) ) = if ( 𝜑 , ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) )
5		iffalse	⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐵 , 𝐶 ) = 𝐶 )
6	5	mpteq2dv	⊢ ( ¬ 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝜑 , 𝐵 , 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
7		iffalse	⊢ ( ¬ 𝜑 → if ( 𝜑 , ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
8	6 7	eqtr4d	⊢ ( ¬ 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝜑 , 𝐵 , 𝐶 ) ) = if ( 𝜑 , ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) )
9	4 8	pm2.61i	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝜑 , 𝐵 , 𝐶 ) ) = if ( 𝜑 , ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )