Theorem 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	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		uncom	⊢ ( 𝐹 ∪ 𝐺 ) = ( 𝐺 ∪ 𝐹 )
2	1	fveq1i	⊢ ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐺 ∪ 𝐹 ) ‘ 𝑋 )
3		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
4	3	eqeq1i	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐵 ∩ 𝐴 ) = ∅ )
5	4	anbi1i	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐵 ) ↔ ( ( 𝐵 ∩ 𝐴 ) = ∅ ∧ 𝑋 ∈ 𝐵 ) )
6		fvun1	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐹 Fn 𝐴 ∧ ( ( 𝐵 ∩ 𝐴 ) = ∅ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝐺 ∪ 𝐹 ) ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
7	5 6	syl3an3b	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐹 Fn 𝐴 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝐺 ∪ 𝐹 ) ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
8	7	3com12	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝐺 ∪ 𝐹 ) ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
9	2 8	syl5eq	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )