This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝜑 , ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )