Theorem ituni0

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

	Ref	Expression
Hypothesis	ituni.u	|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
Assertion	ituni0	|- ( A e. V -> ( ( U ` A ) ` (/) ) = A )

Proof

Step	Hyp	Ref	Expression
1		ituni.u	|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
2	1	itunifval	|- ( A e. V -> ( U ` A ) = ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) )
3	2	fveq1d	|- ( A e. V -> ( ( U ` A ) ` (/) ) = ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` (/) ) )
4		fr0g	|- ( A e. V -> ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` (/) ) = A )
5	3 4	eqtrd	|- ( A e. V -> ( ( U ` A ) ` (/) ) = A )