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	$$⊢y\in A\to \forall xy\in A$$
Assertion	bnj1400	$$⊢\mathrm{dom}\bigcup A=\bigcup _{x\in A}\mathrm{dom}x$$

Proof

Step	Hyp	Ref	Expression
1		bnj1400.1	$$⊢y\in A\to \forall xy\in A$$
2		dmuni	$$⊢\mathrm{dom}\bigcup A=\bigcup _{z\in A}\mathrm{dom}z$$
3		df-iun	$$⊢\bigcup _{x\in A}\mathrm{dom}x=\left\{y|\exists x\in Ay\in \mathrm{dom}x\right\}$$
4		df-iun	$$⊢\bigcup _{z\in A}\mathrm{dom}z=\left\{y|\exists z\in Ay\in \mathrm{dom}z\right\}$$
5	1	nfcii	$$⊢\underset{\_}{Ⅎ}xA$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}zA$$
7		nfv	$$⊢Ⅎzy\in \mathrm{dom}x$$
8		nfv	$$⊢Ⅎxy\in \mathrm{dom}z$$
9		dmeq	$$⊢x=z\to \mathrm{dom}x=\mathrm{dom}z$$
10	9	eleq2d	$$⊢x=z\to \left(y\in \mathrm{dom}x\leftrightarrow y\in \mathrm{dom}z\right)$$
11	5 6 7 8 10	cbvrexfw	$$⊢\exists x\in Ay\in \mathrm{dom}x\leftrightarrow \exists z\in Ay\in \mathrm{dom}z$$
12	11	abbii	$$⊢\left\{y|\exists x\in Ay\in \mathrm{dom}x\right\}=\left\{y|\exists z\in Ay\in \mathrm{dom}z\right\}$$
13	4 12	eqtr4i	$$⊢\bigcup _{z\in A}\mathrm{dom}z=\left\{y|\exists x\in Ay\in \mathrm{dom}x\right\}$$
14	3 13	eqtr4i	$$⊢\bigcup _{x\in A}\mathrm{dom}x=\bigcup _{z\in A}\mathrm{dom}z$$
15	2 14	eqtr4i	$$⊢\mathrm{dom}\bigcup A=\bigcup _{x\in A}\mathrm{dom}x$$