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 e. A |-> if ( ph , B , C ) ) = if ( ph , ( x e. A |-> B ) , ( x e. A |-> C ) )

Proof

Step	Hyp	Ref	Expression
1		iftrue	|- ( ph -> if ( ph , B , C ) = B )
2	1	mpteq2dv	|- ( ph -> ( x e. A |-> if ( ph , B , C ) ) = ( x e. A |-> B ) )
3		iftrue	|- ( ph -> if ( ph , ( x e. A |-> B ) , ( x e. A |-> C ) ) = ( x e. A |-> B ) )
4	2 3	eqtr4d	|- ( ph -> ( x e. A |-> if ( ph , B , C ) ) = if ( ph , ( x e. A |-> B ) , ( x e. A |-> C ) ) )
5		iffalse	|- ( -. ph -> if ( ph , B , C ) = C )
6	5	mpteq2dv	|- ( -. ph -> ( x e. A |-> if ( ph , B , C ) ) = ( x e. A |-> C ) )
7		iffalse	|- ( -. ph -> if ( ph , ( x e. A |-> B ) , ( x e. A |-> C ) ) = ( x e. A |-> C ) )
8	6 7	eqtr4d	|- ( -. ph -> ( x e. A |-> if ( ph , B , C ) ) = if ( ph , ( x e. A |-> B ) , ( x e. A |-> C ) ) )
9	4 8	pm2.61i	|- ( x e. A |-> if ( ph , B , C ) ) = if ( ph , ( x e. A |-> B ) , ( x e. A |-> C ) )