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 e. A | ph }
Assertion	partfun2	|- ( x e. A |-> if ( ph , B , C ) ) = ( ( x e. D |-> B ) u. ( x e. ( A \ D ) |-> C ) )

Proof

Step	Hyp	Ref	Expression
1		partfun2.1	|- D = { x e. A | ph }
2		partfun	|- ( x e. A |-> if ( x e. D , B , C ) ) = ( ( x e. ( A i^i D ) |-> B ) u. ( x e. ( A \ D ) |-> C ) )
3	1	reqabi	|- ( x e. D <-> ( x e. A /\ ph ) )
4	3	baib	|- ( x e. A -> ( x e. D <-> ph ) )
5	4	ifbid	|- ( x e. A -> if ( x e. D , B , C ) = if ( ph , B , C ) )
6	5	mpteq2ia	|- ( x e. A |-> if ( x e. D , B , C ) ) = ( x e. A |-> if ( ph , B , C ) )
7	1	ssrab3	|- D C_ A
8		sseqin2	|- ( D C_ A <-> ( A i^i D ) = D )
9	7 8	mpbi	|- ( A i^i D ) = D
10	9	mpteq1i	|- ( x e. ( A i^i D ) |-> B ) = ( x e. D |-> B )
11	10	uneq1i	|- ( ( x e. ( A i^i D ) |-> B ) u. ( x e. ( A \ D ) |-> C ) ) = ( ( x e. D |-> B ) u. ( x e. ( A \ D ) |-> C ) )
12	2 6 11	3eqtr3i	|- ( x e. A |-> if ( ph , B , C ) ) = ( ( x e. D |-> B ) u. ( x e. ( A \ D ) |-> C ) )