Theorem relbigcup

Description: The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Assertion	relbigcup	|- Rel Bigcup

Proof

Step	Hyp	Ref	Expression
1		relxp	|- Rel ( _V X. _V )
2		reldif	|- ( Rel ( _V X. _V ) -> Rel ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) ) )
3	1 2	ax-mp	|- Rel ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) )
4		df-bigcup	|- Bigcup = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) )
5	4	releqi	|- ( Rel Bigcup <-> Rel ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) ) )
6	3 5	mpbir	|- Rel Bigcup