Metamath Proof Explorer

Theorem ifexg

Description: Conditional operator existence. (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 elex 
 |-  ( A e. V -> A e. _V )
2 elex 
 |-  ( B e. W -> B e. _V )
3 ifcl 
 |-  ( ( A e. _V /\ B e. _V ) -> if ( ph , A , B ) e. _V )
4 1 2 3 syl2an 
 |-  ( ( A e. V /\ B e. W ) -> if ( ph , A , B ) e. _V )