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

Metamath Proof Explorer

Theorem ifel

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

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

Proof

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