Metamath Proof Explorer

Theorem elif

Description: Membership in a conditional operator. (Contributed by NM, 14-Feb-2005)

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

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

Step

Hyp

Ref

Expression

 |-  ( if ( ph , B , C ) = B -> ( A e. if ( ph , B , C ) <-> A e. B ) )

 |-  ( if ( ph , B , C ) = C -> ( A e. if ( ph , B , C ) <-> A e. C ) )

1 2

 |-  ( A e. if ( ph , B , C ) <-> ( ( ph /\ A e. B ) \/ ( -. ph /\ A e. C ) ) )