This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjimxrnres

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

		Ref	Expression
	Assertion	disjimxrnres	⊢ ( Disj 𝑆 → Disj ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) )

Step	Hyp	Ref	Expression
1		disjimres	⊢ ( Disj 𝑆 → Disj ( 𝑆 ↾ 𝐴 ) )
2		disjimxrn	⊢ ( Disj ( 𝑆 ↾ 𝐴 ) → Disj ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) )
3	1 2	syl	⊢ ( Disj 𝑆 → Disj ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) )