Metamath Proof Explorer

Theorem ifcl

Description: Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005)

Ref Expression
Assertion ifcl 
|- ( ( A e. C /\ B e. C ) -> if ( ph , A , B ) e. C )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( A = if ( ph , A , B ) -> ( A e. C <-> if ( ph , A , B ) e. C ) )
2 eleq1 
 |-  ( B = if ( ph , A , B ) -> ( B e. C <-> if ( ph , A , B ) e. C ) )
3 1 2 ifboth 
 |-  ( ( A e. C /\ B e. C ) -> if ( ph , A , B ) e. C )