This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → F Fn A
fvun1d.2 ⊢ φ → G Fn B
fvun1d.3 ⊢ φ → A ∩ B = ∅
fvun1d.4 ⊢ φ → X ∈ A
Assertion fvun1d ⊢ φ → F ∪ G ⁡ X = F ⁡ X

Proof

Step Hyp Ref Expression
1 fvun1d.1 ⊢ φ → F Fn A
2 fvun1d.2 ⊢ φ → G Fn B
3 fvun1d.3 ⊢ φ → A ∩ B = ∅
4 fvun1d.4 ⊢ φ → X ∈ A
5 3 4 jca ⊢ φ → A ∩ B = ∅ ∧ X ∈ A
6 1 2 5 3jca ⊢ φ → F Fn A ∧ G Fn B ∧ A ∩ B = ∅ ∧ X ∈ A
7 fvun1 ⊢ F Fn A ∧ G Fn B ∧ A ∩ B = ∅ ∧ X ∈ A → F ∪ G ⁡ X = F ⁡ X
8 6 7 syl ⊢ φ → F ∪ G ⁡ X = F ⁡ X