Metamath Proof Explorer

Theorem bnj1386

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1386.1 ⊢ φ ↔ ∀ f ∈ A Fun ⁡ f
bnj1386.2 ⊢ D = dom ⁡ f ∩ dom ⁡ g
bnj1386.3 ⊢ ψ ↔ φ ∧ ∀ f ∈ A ∀ g ∈ A f ↾ D = g ↾ D
bnj1386.4 ⊢ x ∈ A → ∀ f x ∈ A
Assertion bnj1386 ⊢ ψ → Fun ⁡ ⋃ A

Proof

Step Hyp Ref Expression
1 bnj1386.1 ⊢ φ ↔ ∀ f ∈ A Fun ⁡ f
2 bnj1386.2 ⊢ D = dom ⁡ f ∩ dom ⁡ g
3 bnj1386.3 ⊢ ψ ↔ φ ∧ ∀ f ∈ A ∀ g ∈ A f ↾ D = g ↾ D
4 bnj1386.4 ⊢ x ∈ A → ∀ f x ∈ A
5 biid ⊢ ∀ h ∈ A Fun ⁡ h ↔ ∀ h ∈ A Fun ⁡ h
6 eqid ⊢ dom ⁡ h ∩ dom ⁡ g = dom ⁡ h ∩ dom ⁡ g
7 biid ⊢ ∀ h ∈ A Fun ⁡ h ∧ ∀ h ∈ A ∀ g ∈ A h ↾ dom ⁡ h ∩ dom ⁡ g = g ↾ dom ⁡ h ∩ dom ⁡ g ↔ ∀ h ∈ A Fun ⁡ h ∧ ∀ h ∈ A ∀ g ∈ A h ↾ dom ⁡ h ∩ dom ⁡ g = g ↾ dom ⁡ h ∩ dom ⁡ g
8 1 2 3 4 5 6 7 bnj1385 ⊢ ψ → Fun ⁡ ⋃ A