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 → ψ