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 ( 𝜑𝐹 Fn 𝐴 )
fvun1d.2 ( 𝜑𝐺 Fn 𝐵 )
fvun1d.3 ( 𝜑 → ( 𝐴𝐵 ) = ∅ )
fvun1d.4 ( 𝜑𝑋𝐴 )
Assertion fvun1d ( 𝜑 → ( ( 𝐹𝐺 ) ‘ 𝑋 ) = ( 𝐹𝑋 ) )

Proof

Step Hyp Ref Expression
1 fvun1d.1 ( 𝜑𝐹 Fn 𝐴 )
2 fvun1d.2 ( 𝜑𝐺 Fn 𝐵 )
3 fvun1d.3 ( 𝜑 → ( 𝐴𝐵 ) = ∅ )
4 fvun1d.4 ( 𝜑𝑋𝐴 )
5 3 4 jca ( 𝜑 → ( ( 𝐴𝐵 ) = ∅ ∧ 𝑋𝐴 ) )
6 1 2 5 3jca ( 𝜑 → ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ( ( 𝐴𝐵 ) = ∅ ∧ 𝑋𝐴 ) ) )
7 fvun1 ( ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ( ( 𝐴𝐵 ) = ∅ ∧ 𝑋𝐴 ) ) → ( ( 𝐹𝐺 ) ‘ 𝑋 ) = ( 𝐹𝑋 ) )
8 6 7 syl ( 𝜑 → ( ( 𝐹𝐺 ) ‘ 𝑋 ) = ( 𝐹𝑋 ) )