dmres

Description: The domain of a restriction. Exercise 14 of TakeutiZaring p. 25. (Contributed by NM, 1-Aug-1994)

		Ref	Expression
	Assertion	dmres	$⊢ dom ({A ↾}_{B}) = B \cap dom A$

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2	1	eldm2	$⊢ x \in dom ({A ↾}_{B}) \leftrightarrow \exists y ⟨x, y⟩ \in ({A ↾}_{B})$
3		19.42v	$⊢ \exists y (x \in B \land ⟨x, y⟩ \in A) \leftrightarrow (x \in B \land \exists y ⟨x, y⟩ \in A)$
4		vex	$⊢ y \in V$
5	4	opelresi	$⊢ ⟨x, y⟩ \in ({A ↾}_{B}) \leftrightarrow (x \in B \land ⟨x, y⟩ \in A)$
6	5	exbii	$⊢ \exists y ⟨x, y⟩ \in ({A ↾}_{B}) \leftrightarrow \exists y (x \in B \land ⟨x, y⟩ \in A)$
7	1	eldm2	$⊢ x \in dom A \leftrightarrow \exists y ⟨x, y⟩ \in A$
8	7	anbi2i	$⊢ (x \in B \land x \in dom A) \leftrightarrow (x \in B \land \exists y ⟨x, y⟩ \in A)$
9	3 6 8	3bitr4i	$⊢ \exists y ⟨x, y⟩ \in ({A ↾}_{B}) \leftrightarrow (x \in B \land x \in dom A)$
10	2 9	bitr2i	$⊢ (x \in B \land x \in dom A) \leftrightarrow x \in dom ({A ↾}_{B})$
11	10	ineqri	$⊢ B \cap dom A = dom ({A ↾}_{B})$
12	11	eqcomi	$⊢ dom ({A ↾}_{B}) = B \cap dom A$

Metamath Proof Explorer