This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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