Theorem ituni0

Description: A zero-fold iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Hypothesis	ituni.u	$$⊢U=\left(x\in \mathrm{V}⟼{\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),x\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
Assertion	ituni0	$$⊢A\in V\to U\left(A\right)\left(\varnothing \right)=A$$

Proof

Step	Hyp	Ref	Expression
1		ituni.u	$$⊢U=\left(x\in \mathrm{V}⟼{\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),x\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
2	1	itunifval	$$⊢A\in V\to U\left(A\right)={\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),A\right)\upharpoonright }_{\mathrm{\omega }}$$
3	2	fveq1d	$$⊢A\in V\to U\left(A\right)\left(\varnothing \right)=\left({\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),A\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)$$
4		fr0g	$$⊢A\in V\to \left({\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),A\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)=A$$
5	3 4	eqtrd	$$⊢A\in V\to U\left(A\right)\left(\varnothing \right)=A$$