Description: If a statement is true for every element of a class and for every element of its complement relative to a second class, then it is true for every element in the second class. (Contributed by BTernaryTau, 27-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | srcmpltd.1 | ||
srcmpltd.2 | |||
Assertion | srcmpltd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | srcmpltd.1 | ||
2 | srcmpltd.2 | ||
3 | elun2 | ||
4 | undif2 | ||
5 | 3 4 | eleqtrrdi | |
6 | elunant | ||
7 | 1 2 6 | sylanbrc | |
8 | 5 7 | syl5 |