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	$⊢ φ \leftrightarrow \forall f \in A Fun f$
	bnj1383.2	$⊢ D = dom f \cap dom g$
	bnj1383.3	$⊢ ψ \leftrightarrow (φ \land \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D})$
Assertion	bnj1383	$⊢ ψ \to Fun ⋃ A$

Step	Hyp	Ref	Expression
1		bnj1383.1	$⊢ φ \leftrightarrow \forall f \in A Fun f$
2		bnj1383.2	$⊢ D = dom f \cap dom g$
3		bnj1383.3	$⊢ ψ \leftrightarrow (φ \land \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D})$
4		biid	$⊢ (ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \leftrightarrow (ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A)$
5		biid	$⊢ ((ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \land f \in A \land ⟨x, y⟩ \in f) \leftrightarrow ((ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \land f \in A \land ⟨x, y⟩ \in f)$
6		biid	$⊢ (((ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \land f \in A \land ⟨x, y⟩ \in f) \land g \in A \land ⟨x, z⟩ \in g) \leftrightarrow (((ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \land f \in A \land ⟨x, y⟩ \in f) \land g \in A \land ⟨x, z⟩ \in g)$
7	1 2 3 4 5 6	bnj1379	$⊢ ψ \to Fun ⋃ A$

Metamath Proof Explorer