Theorem bnj1400

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

	Ref	Expression
Hypothesis	bnj1400.1	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
Assertion	bnj1400	⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥

Proof

Step	Hyp	Ref	Expression
1		bnj1400.1	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
2		dmuni	⊢ dom ∪ 𝐴 = ∪ 𝑧 ∈ 𝐴 dom 𝑧
3		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 dom 𝑥 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 }
4		df-iun	⊢ ∪ 𝑧 ∈ 𝐴 dom 𝑧 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ dom 𝑧 }
5	1	nfcii	⊢ Ⅎ 𝑥 𝐴
6		nfcv	⊢ Ⅎ 𝑧 𝐴
7		nfv	⊢ Ⅎ 𝑧 𝑦 ∈ dom 𝑥
8		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ dom 𝑧
9		dmeq	⊢ ( 𝑥 = 𝑧 → dom 𝑥 = dom 𝑧 )
10	9	eleq2d	⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ dom 𝑥 ↔ 𝑦 ∈ dom 𝑧 ) )
11	5 6 7 8 10	cbvrexfw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ dom 𝑧 )
12	11	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 } = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ dom 𝑧 }
13	4 12	eqtr4i	⊢ ∪ 𝑧 ∈ 𝐴 dom 𝑧 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 }
14	3 13	eqtr4i	⊢ ∪ 𝑥 ∈ 𝐴 dom 𝑥 = ∪ 𝑧 ∈ 𝐴 dom 𝑧
15	2 14	eqtr4i	⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥