# 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
`|- ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. B ) ) -> ( ( F u. G ) ` X ) = ( G ` X ) )`

### Proof

Step Hyp Ref Expression
1 uncom
` |-  ( F u. G ) = ( G u. F )`
2 1 fveq1i
` |-  ( ( F u. G ) ` X ) = ( ( G u. F ) ` X )`
3 incom
` |-  ( A i^i B ) = ( B i^i A )`
4 3 eqeq1i
` |-  ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )`
5 4 anbi1i
` |-  ( ( ( A i^i B ) = (/) /\ X e. B ) <-> ( ( B i^i A ) = (/) /\ X e. B ) )`
6 fvun1
` |-  ( ( G Fn B /\ F Fn A /\ ( ( B i^i A ) = (/) /\ X e. B ) ) -> ( ( G u. F ) ` X ) = ( G ` X ) )`
7 5 6 syl3an3b
` |-  ( ( G Fn B /\ F Fn A /\ ( ( A i^i B ) = (/) /\ X e. B ) ) -> ( ( G u. F ) ` X ) = ( G ` X ) )`
8 7 3com12
` |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. B ) ) -> ( ( G u. F ) ` X ) = ( G ` X ) )`
9 2 8 syl5eq
` |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. B ) ) -> ( ( F u. G ) ` X ) = ( G ` X ) )`