Theorem ifel

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

	Ref	Expression
Assertion	ifel	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) ∈ 𝐶 ↔ ( ( 𝜑 ∧ 𝐴 ∈ 𝐶 ) ∨ ( ¬ 𝜑 ∧ 𝐵 ∈ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 → ( if ( 𝜑 , 𝐴 , 𝐵 ) ∈ 𝐶 ↔ 𝐴 ∈ 𝐶 ) )
2		eleq1	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 → ( if ( 𝜑 , 𝐴 , 𝐵 ) ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
3	1 2	elimif	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) ∈ 𝐶 ↔ ( ( 𝜑 ∧ 𝐴 ∈ 𝐶 ) ∨ ( ¬ 𝜑 ∧ 𝐵 ∈ 𝐶 ) ) )