This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elif

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

Ref Expression
Assertion elif ⊢ A ∈ if φ B C ↔ φ ∧ A ∈ B ∨ ¬ φ ∧ A ∈ C

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ if φ B C = B → A ∈ if φ B C ↔ A ∈ B
2 eleq2 ⊢ if φ B C = C → A ∈ if φ B C ↔ A ∈ C
3 1 2 elimif ⊢ A ∈ if φ B C ↔ φ ∧ A ∈ B ∨ ¬ φ ∧ A ∈ C