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 
|- ( 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 ) )