Theorem cnvuni

Description: The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004)

	Ref	Expression
Assertion	cnvuni	|- `' U. A = U_ x e. A `' x

Proof

Step	Hyp	Ref	Expression
1		elcnv2	|- ( y e. `' U. A <-> E. z E. w ( y = <. z , w >. /\ <. w , z >. e. U. A ) )
2		eluni2	|- ( <. w , z >. e. U. A <-> E. x e. A <. w , z >. e. x )
3	2	anbi2i	|- ( ( y = <. z , w >. /\ <. w , z >. e. U. A ) <-> ( y = <. z , w >. /\ E. x e. A <. w , z >. e. x ) )
4		r19.42v	|- ( E. x e. A ( y = <. z , w >. /\ <. w , z >. e. x ) <-> ( y = <. z , w >. /\ E. x e. A <. w , z >. e. x ) )
5	3 4	bitr4i	|- ( ( y = <. z , w >. /\ <. w , z >. e. U. A ) <-> E. x e. A ( y = <. z , w >. /\ <. w , z >. e. x ) )
6	5	2exbii	|- ( E. z E. w ( y = <. z , w >. /\ <. w , z >. e. U. A ) <-> E. z E. w E. x e. A ( y = <. z , w >. /\ <. w , z >. e. x ) )
7		elcnv2	|- ( y e. `' x <-> E. z E. w ( y = <. z , w >. /\ <. w , z >. e. x ) )
8	7	rexbii	|- ( E. x e. A y e. `' x <-> E. x e. A E. z E. w ( y = <. z , w >. /\ <. w , z >. e. x ) )
9		rexcom4	|- ( E. x e. A E. z E. w ( y = <. z , w >. /\ <. w , z >. e. x ) <-> E. z E. x e. A E. w ( y = <. z , w >. /\ <. w , z >. e. x ) )
10		rexcom4	|- ( E. x e. A E. w ( y = <. z , w >. /\ <. w , z >. e. x ) <-> E. w E. x e. A ( y = <. z , w >. /\ <. w , z >. e. x ) )
11	10	exbii	|- ( E. z E. x e. A E. w ( y = <. z , w >. /\ <. w , z >. e. x ) <-> E. z E. w E. x e. A ( y = <. z , w >. /\ <. w , z >. e. x ) )
12	8 9 11	3bitrri	|- ( E. z E. w E. x e. A ( y = <. z , w >. /\ <. w , z >. e. x ) <-> E. x e. A y e. `' x )
13	1 6 12	3bitri	|- ( y e. `' U. A <-> E. x e. A y e. `' x )
14		eliun	|- ( y e. U_ x e. A `' x <-> E. x e. A y e. `' x )
15	13 14	bitr4i	|- ( y e. `' U. A <-> y e. U_ x e. A `' x )
16	15	eqriv	|- `' U. A = U_ x e. A `' x