Metamath Proof Explorer

Theorem ifexg

Description: Existence of the conditional operator (closed form). (Contributed by NM, 21-Mar-2011) (Proof shortened by BJ, 1-Sep-2022)

Ref Expression
Assertion ifexg 
|- ( ( A e. V /\ B e. W ) -> if ( ph , A , B ) e. _V )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. V /\ B e. W ) -> A e. V )
2 simpr 
 |-  ( ( A e. V /\ B e. W ) -> B e. W )
3 1 2 ifexd 
 |-  ( ( A e. V /\ B e. W ) -> if ( ph , A , B ) e. _V )