Metamath Proof Explorer

Theorem fvreseq0

Description: Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019)

		Ref	Expression
	Assertion	fvreseq0	$⊢ ((F Fn A \land G Fn C) \land (B \subseteq A \land B \subseteq C)) \to ({F ↾}_{B} = {G ↾}_{B} \leftrightarrow \forall x \in B F (x) = G (x))$

Proof

Step	Hyp	Ref	Expression
1		fnssres	$⊢ (F Fn A \land B \subseteq A) \to ({F ↾}_{B}) Fn B$
2		fnssres	$⊢ (G Fn C \land B \subseteq C) \to ({G ↾}_{B}) Fn B$
3		eqfnfv	$⊢ (({F ↾}_{B}) Fn B \land ({G ↾}_{B}) Fn B) \to ({F ↾}_{B} = {G ↾}_{B} \leftrightarrow \forall x \in B ({F ↾}_{B}) (x) = ({G ↾}_{B}) (x))$
4		fvres	$⊢ x \in B \to ({F ↾}_{B}) (x) = F (x)$
5		fvres	$⊢ x \in B \to ({G ↾}_{B}) (x) = G (x)$
6	4 5	eqeq12d	$⊢ x \in B \to (({F ↾}_{B}) (x) = ({G ↾}_{B}) (x) \leftrightarrow F (x) = G (x))$
7	6	ralbiia	$⊢ \forall x \in B ({F ↾}_{B}) (x) = ({G ↾}_{B}) (x) \leftrightarrow \forall x \in B F (x) = G (x)$
8	3 7	bitrdi	$⊢ (({F ↾}_{B}) Fn B \land ({G ↾}_{B}) Fn B) \to ({F ↾}_{B} = {G ↾}_{B} \leftrightarrow \forall x \in B F (x) = G (x))$
9	1 2 8	syl2an	$⊢ ((F Fn A \land B \subseteq A) \land (G Fn C \land B \subseteq C)) \to ({F ↾}_{B} = {G ↾}_{B} \leftrightarrow \forall x \in B F (x) = G (x))$
10	9	an4s	$⊢ ((F Fn A \land G Fn C) \land (B \subseteq A \land B \subseteq C)) \to ({F ↾}_{B} = {G ↾}_{B} \leftrightarrow \forall x \in B F (x) = G (x))$