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	⊢ ( 𝐴 ∈ if ( 𝜑 , 𝐵 , ∅ ) ↔ ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elif	⊢ ( 𝐴 ∈ if ( 𝜑 , 𝐵 , ∅ ) ↔ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) ∨ ( ¬ 𝜑 ∧ 𝐴 ∈ ∅ ) ) )
2		noel	⊢ ¬ 𝐴 ∈ ∅
3	2	intnan	⊢ ¬ ( ¬ 𝜑 ∧ 𝐴 ∈ ∅ )
4	3	biorfri	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) ∨ ( ¬ 𝜑 ∧ 𝐴 ∈ ∅ ) ) )
5	1 4	bitr4i	⊢ ( 𝐴 ∈ if ( 𝜑 , 𝐵 , ∅ ) ↔ ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) )