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	⊢ ( 𝜑 ↔ ∀ 𝑓 ∈ 𝐴 Fun 𝑓 )
	bnj1386.2	⊢ 𝐷 = ( dom 𝑓 ∩ dom 𝑔 )
	bnj1386.3	⊢ ( 𝜓 ↔ ( 𝜑 ∧ ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ) )
	bnj1386.4	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑓 𝑥 ∈ 𝐴 )
Assertion	bnj1386	⊢ ( 𝜓 → Fun ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bnj1386.1	⊢ ( 𝜑 ↔ ∀ 𝑓 ∈ 𝐴 Fun 𝑓 )
2		bnj1386.2	⊢ 𝐷 = ( dom 𝑓 ∩ dom 𝑔 )
3		bnj1386.3	⊢ ( 𝜓 ↔ ( 𝜑 ∧ ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ) )
4		bnj1386.4	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑓 𝑥 ∈ 𝐴 )
5		biid	⊢ ( ∀ ℎ ∈ 𝐴 Fun ℎ ↔ ∀ ℎ ∈ 𝐴 Fun ℎ )
6		eqid	⊢ ( dom ℎ ∩ dom 𝑔 ) = ( dom ℎ ∩ dom 𝑔 )
7		biid	⊢ ( ( ∀ ℎ ∈ 𝐴 Fun ℎ ∧ ∀ ℎ ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ ( dom ℎ ∩ dom 𝑔 ) ) = ( 𝑔 ↾ ( dom ℎ ∩ dom 𝑔 ) ) ) ↔ ( ∀ ℎ ∈ 𝐴 Fun ℎ ∧ ∀ ℎ ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ ( dom ℎ ∩ dom 𝑔 ) ) = ( 𝑔 ↾ ( dom ℎ ∩ dom 𝑔 ) ) ) )
8	1 2 3 4 5 6 7	bnj1385	⊢ ( 𝜓 → Fun ∪ 𝐴 )