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φABAB

Proof

Step Hyp Ref Expression
1 eqid x|φ=x|φ
2 1 dfif4 ifφAB=ABAVx|φBx|φ
3 inss1 ABAVx|φBx|φAB
4 2 3 eqsstri ifφABAB