imaindm

Description: The image is unaffected by intersection with the domain. (Contributed by Scott Fenton, 17-Dec-2021)

		Ref	Expression
	Assertion	imaindm	$⊢ R [A] = R [A \cap dom R]$

Step	Hyp	Ref	Expression
1		vex	$⊢ y \in V$
2		vex	$⊢ x \in V$
3	1 2	breldm	$⊢ y R x \to y \in dom R$
4	3	pm4.71ri	$⊢ y R x \leftrightarrow (y \in dom R \land y R x)$
5	4	rexbii	$⊢ \exists y \in A y R x \leftrightarrow \exists y \in A (y \in dom R \land y R x)$
6		rexin	$⊢ \exists y \in (A \cap dom R) y R x \leftrightarrow \exists y \in A (y \in dom R \land y R x)$
7	5 6	bitr4i	$⊢ \exists y \in A y R x \leftrightarrow \exists y \in (A \cap dom R) y R x$
8	2	elima	$⊢ x \in R [A] \leftrightarrow \exists y \in A y R x$
9	2	elima	$⊢ x \in R [A \cap dom R] \leftrightarrow \exists y \in (A \cap dom R) y R x$
10	7 8 9	3bitr4i	$⊢ x \in R [A] \leftrightarrow x \in R [A \cap dom R]$
11	10	eqriv	$⊢ R [A] = R [A \cap dom R]$

Metamath Proof Explorer