Description: A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | ifssun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | 1 | dfif4 | |
3 | inss1 | |
|
4 | 2 3 | eqsstri | |