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

Metamath Proof Explorer

Theorem resdmdfsn

Description: Restricting a relation to its domain without a set is the same as restricting the relation to the universe without this set. (Contributed by AV, 2-Dec-2018)

		Ref	Expression
	Assertion	resdmdfsn	$⊢ Rel R \to {R ↾}_{(V ∖ \{X\})} = {R ↾}_{(dom R ∖ \{X\})}$

Proof

Step	Hyp	Ref	Expression
1		resindm	$⊢ Rel R \to {R ↾}_{((V ∖ \{X\}) \cap dom R)} = {R ↾}_{(V ∖ \{X\})}$
2		indif1	$⊢ (V ∖ \{X\}) \cap dom R = (V \cap dom R) ∖ \{X\}$
3		incom	$⊢ V \cap dom R = dom R \cap V$
4		inv1	$⊢ dom R \cap V = dom R$
5	3 4	eqtri	$⊢ V \cap dom R = dom R$
6	5	difeq1i	$⊢ (V \cap dom R) ∖ \{X\} = dom R ∖ \{X\}$
7	2 6	eqtri	$⊢ (V ∖ \{X\}) \cap dom R = dom R ∖ \{X\}$
8	7	reseq2i	$⊢ {R ↾}_{((V ∖ \{X\}) \cap dom R)} = {R ↾}_{(dom R ∖ \{X\})}$
9	1 8	eqtr3di	$⊢ Rel R \to {R ↾}_{(V ∖ \{X\})} = {R ↾}_{(dom R ∖ \{X\})}$