Metamath Proof Explorer


Theorem ifssun

Description: A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024)

Ref Expression
Assertion ifssun if φ A B A B

Proof

Step Hyp Ref Expression
1 eqid x | φ = x | φ
2 1 dfif4 if φ A B = A B A V x | φ B x | φ
3 inss1 A B A V x | φ B x | φ A B
4 2 3 eqsstri if φ A B A B