Metamath Proof Explorer

Theorem partfun2

Description: Rewrite a function defined by parts, using a mapping and an if construct, into a union of functions on disjoint domains. See also partfun and ifmpt2v . (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypothesis partfun2.1 ⊢ D = x ∈ A | φ
Assertion partfun2 ⊢ x ∈ A ⟼ if φ B C = x ∈ D ⟼ B ∪ x ∈ A ∖ D ⟼ C

Proof

Step Hyp Ref Expression
1 partfun2.1 ⊢ D = x ∈ A | φ
2 partfun ⊢ x ∈ A ⟼ if x ∈ D B C = x ∈ A ∩ D ⟼ B ∪ x ∈ A ∖ D ⟼ C
3 1 reqabi ⊢ x ∈ D ↔ x ∈ A ∧ φ
4 3 baib ⊢ x ∈ A → x ∈ D ↔ φ
5 4 ifbid ⊢ x ∈ A → if x ∈ D B C = if φ B C
6 5 mpteq2ia ⊢ x ∈ A ⟼ if x ∈ D B C = x ∈ A ⟼ if φ B C
7 1 ssrab3 ⊢ D ⊆ A
8 sseqin2 ⊢ D ⊆ A ↔ A ∩ D = D
9 7 8 mpbi ⊢ A ∩ D = D
10 9 mpteq1i ⊢ x ∈ A ∩ D ⟼ B = x ∈ D ⟼ B
11 10 uneq1i ⊢ x ∈ A ∩ D ⟼ B ∪ x ∈ A ∖ D ⟼ C = x ∈ D ⟼ B ∪ x ∈ A ∖ D ⟼ C
12 2 6 11 3eqtr3i ⊢ x ∈ A ⟼ if φ B C = x ∈ D ⟼ B ∪ x ∈ A ∖ D ⟼ C