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 e. if ( ph , B , (/) ) <-> ( ph /\ A e. B ) )

Proof

Step	Hyp	Ref	Expression
1		elif	|- ( A e. if ( ph , B , (/) ) <-> ( ( ph /\ A e. B ) \/ ( -. ph /\ A e. (/) ) ) )
2		noel	|- -. A e. (/)
3	2	intnan	|- -. ( -. ph /\ A e. (/) )
4	3	biorfri	|- ( ( ph /\ A e. B ) <-> ( ( ph /\ A e. B ) \/ ( -. ph /\ A e. (/) ) ) )
5	1 4	bitr4i	|- ( A e. if ( ph , B , (/) ) <-> ( ph /\ A e. B ) )