Metamath Proof Explorer

Theorem ifel

Description: Membership of a conditional operator. (Contributed by NM, 10-Sep-2005)

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

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

Step

Hyp

Ref

Expression

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

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

1 2

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