Theorem fvun2d

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

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

Proof

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