# 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 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {B}\right)\right)\to \left({F}\cup {G}\right)\left({X}\right)={G}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 uncom ${⊢}{F}\cup {G}={G}\cup {F}$
2 1 fveq1i ${⊢}\left({F}\cup {G}\right)\left({X}\right)=\left({G}\cup {F}\right)\left({X}\right)$
3 incom ${⊢}{A}\cap {B}={B}\cap {A}$
4 3 eqeq1i ${⊢}{A}\cap {B}=\varnothing ↔{B}\cap {A}=\varnothing$
5 4 anbi1i ${⊢}\left({A}\cap {B}=\varnothing \wedge {X}\in {B}\right)↔\left({B}\cap {A}=\varnothing \wedge {X}\in {B}\right)$
6 fvun1 ${⊢}\left({G}Fn{B}\wedge {F}Fn{A}\wedge \left({B}\cap {A}=\varnothing \wedge {X}\in {B}\right)\right)\to \left({G}\cup {F}\right)\left({X}\right)={G}\left({X}\right)$
7 5 6 syl3an3b ${⊢}\left({G}Fn{B}\wedge {F}Fn{A}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {B}\right)\right)\to \left({G}\cup {F}\right)\left({X}\right)={G}\left({X}\right)$
8 7 3com12 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {B}\right)\right)\to \left({G}\cup {F}\right)\left({X}\right)={G}\left({X}\right)$
9 2 8 syl5eq ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {B}\right)\right)\to \left({F}\cup {G}\right)\left({X}\right)={G}\left({X}\right)$