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 ⊢ x ∈ A ⟼ if φ B C = if φ x ∈ A ⟼ B x ∈ A ⟼ C

Proof

Step Hyp Ref Expression
1 iftrue ⊢ φ → if φ B C = B
2 1 mpteq2dv ⊢ φ → x ∈ A ⟼ if φ B C = x ∈ A ⟼ B
3 iftrue ⊢ φ → if φ x ∈ A ⟼ B x ∈ A ⟼ C = x ∈ A ⟼ B
4 2 3 eqtr4d ⊢ φ → x ∈ A ⟼ if φ B C = if φ x ∈ A ⟼ B x ∈ A ⟼ C
5 iffalse ⊢ ¬ φ → if φ B C = C
6 5 mpteq2dv ⊢ ¬ φ → x ∈ A ⟼ if φ B C = x ∈ A ⟼ C
7 iffalse ⊢ ¬ φ → if φ x ∈ A ⟼ B x ∈ A ⟼ C = x ∈ A ⟼ C
8 6 7 eqtr4d ⊢ ¬ φ → x ∈ A ⟼ if φ B C = if φ x ∈ A ⟼ B x ∈ A ⟼ C
9 4 8 pm2.61i ⊢ x ∈ A ⟼ if φ B C = if φ x ∈ A ⟼ B x ∈ A ⟼ C