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 | ⊢ ( 𝜑 → ( 𝐶 ∈ 𝐵 → 𝜓 ) ) |