# Metamath Proof Explorer

## Theorem bnj1383

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

Ref Expression
Hypotheses bnj1383.1 ${⊢}{\phi }↔\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
bnj1383.2 ${⊢}{D}=\mathrm{dom}{f}\cap \mathrm{dom}{g}$
bnj1383.3 ${⊢}{\psi }↔\left({\phi }\wedge \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)$
Assertion bnj1383 ${⊢}{\psi }\to \mathrm{Fun}\bigcup {A}$

### Proof

Step Hyp Ref Expression
1 bnj1383.1 ${⊢}{\phi }↔\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
2 bnj1383.2 ${⊢}{D}=\mathrm{dom}{f}\cap \mathrm{dom}{g}$
3 bnj1383.3 ${⊢}{\psi }↔\left({\phi }\wedge \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)$
4 biid ${⊢}\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)↔\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)$
5 biid ${⊢}\left(\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)\wedge {f}\in {A}\wedge ⟨{x},{y}⟩\in {f}\right)↔\left(\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)\wedge {f}\in {A}\wedge ⟨{x},{y}⟩\in {f}\right)$
6 biid ${⊢}\left(\left(\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)\wedge {f}\in {A}\wedge ⟨{x},{y}⟩\in {f}\right)\wedge {g}\in {A}\wedge ⟨{x},{z}⟩\in {g}\right)↔\left(\left(\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)\wedge {f}\in {A}\wedge ⟨{x},{y}⟩\in {f}\right)\wedge {g}\in {A}\wedge ⟨{x},{z}⟩\in {g}\right)$
7 1 2 3 4 5 6 bnj1379 ${⊢}{\psi }\to \mathrm{Fun}\bigcup {A}$