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

Metamath Proof Explorer

Theorem unfid

Description: The union of two finite sets is finite. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses unfid.1 ⊢ φ → A ∈ Fin
unfid.2 ⊢ φ → B ∈ Fin
Assertion unfid ⊢ φ → A ∪ B ∈ Fin

Proof

Step Hyp Ref Expression
1 unfid.1 ⊢ φ → A ∈ Fin
2 unfid.2 ⊢ φ → B ∈ Fin
3 unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin
4 1 2 3 syl2anc ⊢ φ → A ∪ B ∈ Fin