Metamath Proof Explorer


Theorem fvun1d

Description: The value of a union when the argument is in the first domain, a deduction version. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses fvun1d.1
|- ( ph -> F Fn A )
fvun1d.2
|- ( ph -> G Fn B )
fvun1d.3
|- ( ph -> ( A i^i B ) = (/) )
fvun1d.4
|- ( ph -> X e. A )
Assertion fvun1d
|- ( ph -> ( ( F u. G ) ` X ) = ( F ` X ) )

Proof

Step Hyp Ref Expression
1 fvun1d.1
 |-  ( ph -> F Fn A )
2 fvun1d.2
 |-  ( ph -> G Fn B )
3 fvun1d.3
 |-  ( ph -> ( A i^i B ) = (/) )
4 fvun1d.4
 |-  ( ph -> X e. A )
5 3 4 jca
 |-  ( ph -> ( ( A i^i B ) = (/) /\ X e. A ) )
6 1 2 5 3jca
 |-  ( ph -> ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) )
7 fvun1
 |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> ( ( F u. G ) ` X ) = ( F ` X ) )
8 6 7 syl
 |-  ( ph -> ( ( F u. G ) ` X ) = ( F ` X ) )