Metamath Proof Explorer


Theorem disjiminres

Description: Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021)

Ref Expression
Assertion disjiminres ( Disj 𝑆 → Disj ( 𝑅 ∩ ( 𝑆𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 disjimres ( Disj 𝑆 → Disj ( 𝑆𝐴 ) )
2 disjimin ( Disj ( 𝑆𝐴 ) → Disj ( 𝑅 ∩ ( 𝑆𝐴 ) ) )
3 1 2 syl ( Disj 𝑆 → Disj ( 𝑅 ∩ ( 𝑆𝐴 ) ) )