Theorem briunov2

Description: Two classes related by the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the two classes are related by that operator value. (Contributed by RP, 1-Jun-2020)

	Ref	Expression
Hypothesis	briunov2.def	|- C = ( r e. _V |-> U_ n e. N ( r .^ n ) )
Assertion	briunov2	|- ( ( R e. U /\ N e. V ) -> ( X ( C ` R ) Y <-> E. n e. N X ( R .^ n ) Y ) )

Proof

Step	Hyp	Ref	Expression
1		briunov2.def	|- C = ( r e. _V |-> U_ n e. N ( r .^ n ) )
2	1	eliunov2	|- ( ( R e. U /\ N e. V ) -> ( <. X , Y >. e. ( C ` R ) <-> E. n e. N <. X , Y >. e. ( R .^ n ) ) )
3		df-br	|- ( X ( C ` R ) Y <-> <. X , Y >. e. ( C ` R ) )
4		df-br	|- ( X ( R .^ n ) Y <-> <. X , Y >. e. ( R .^ n ) )
5	4	rexbii	|- ( E. n e. N X ( R .^ n ) Y <-> E. n e. N <. X , Y >. e. ( R .^ n ) )
6	2 3 5	3bitr4g	|- ( ( R e. U /\ N e. V ) -> ( X ( C ` R ) Y <-> E. n e. N X ( R .^ n ) Y ) )