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