fvun2

Description: The value of a union when the argument is in the second domain. (Contributed by Scott Fenton, 29-Jun-2013)

		Ref	Expression
	Assertion	fvun2	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in B)) \to (F \cup G) (X) = G (X)$

Step	Hyp	Ref	Expression
1		uncom	$⊢ F \cup G = G \cup F$
2	1	fveq1i	$⊢ (F \cup G) (X) = (G \cup F) (X)$
3		incom	$⊢ A \cap B = B \cap A$
4	3	eqeq1i	$⊢ A \cap B = \emptyset \leftrightarrow B \cap A = \emptyset$
5	4	anbi1i	$⊢ (A \cap B = \emptyset \land X \in B) \leftrightarrow (B \cap A = \emptyset \land X \in B)$
6		fvun1	$⊢ (G Fn B \land F Fn A \land (B \cap A = \emptyset \land X \in B)) \to (G \cup F) (X) = G (X)$
7	5 6	syl3an3b	$⊢ (G Fn B \land F Fn A \land (A \cap B = \emptyset \land X \in B)) \to (G \cup F) (X) = G (X)$
8	7	3com12	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in B)) \to (G \cup F) (X) = G (X)$
9	2 8	eqtrid	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in B)) \to (F \cup G) (X) = G (X)$

Metamath Proof Explorer