Metamath Proof Explorer

Theorem elmapresaunres2

Description: fresaunres2 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014)

		Ref	Expression
	Assertion	elmapresaunres2	$⊢ (F \in (C^{A}) \land G \in (C^{B}) \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to {(F \cup G) ↾}_{B} = G$

Step	Hyp	Ref	Expression
1		elmapi	$⊢ F \in (C^{A}) \to F : A ⟶ C$
2		elmapi	$⊢ G \in (C^{B}) \to G : B ⟶ C$
3		id	$⊢ {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)} \to {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}$
4		fresaunres2	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to {(F \cup G) ↾}_{B} = G$
5	1 2 3 4	syl3an	$⊢ (F \in (C^{A}) \land G \in (C^{B}) \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to {(F \cup G) ↾}_{B} = G$