Metamath Proof Explorer


Theorem srcmpltd

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 φ C A ψ
srcmpltd.2 φ C B A ψ
Assertion srcmpltd φ C B ψ

Proof

Step Hyp Ref Expression
1 srcmpltd.1 φ C A ψ
2 srcmpltd.2 φ C B A ψ
3 elun2 C B C A B
4 undif2 A B A = A B
5 3 4 eleqtrrdi C B C A B A
6 elunant C A B A ψ C A ψ C B A ψ
7 1 2 6 sylanbrc φ C A B A ψ
8 5 7 syl5 φ C B ψ