Metamath Proof Explorer

Theorem elif0

Description: Membership in a conditional class with an empty set in the false-branch is equivalent to the condition and membership in the first class. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Assertion elif0 ⊢ A ∈ if φ B ∅ ↔ φ ∧ A ∈ B

Proof

Step Hyp Ref Expression
1 elif ⊢ A ∈ if φ B ∅ ↔ φ ∧ A ∈ B ∨ ¬ φ ∧ A ∈ ∅
2 noel ⊢ ¬ A ∈ ∅
3 2 intnan ⊢ ¬ ¬ φ ∧ A ∈ ∅
4 3 biorfri ⊢ φ ∧ A ∈ B ↔ φ ∧ A ∈ B ∨ ¬ φ ∧ A ∈ ∅
5 1 4 bitr4i ⊢ A ∈ if φ B ∅ ↔ φ ∧ A ∈ B