Theorem uniqsALTV

Description: The union of a quotient set, like uniqs but with a weaker antecedent: only the restricion of R by A needs to be a set, not R itself, see e.g. cnvepima . (Contributed by Peter Mazsa, 20-Jun-2019)

	Ref	Expression
Assertion	uniqsALTV	|- ( ( R |` A ) e. V -> U. ( A /. R ) = ( R " A ) )

Proof

Step	Hyp	Ref	Expression
1		ecex2	|- ( ( R |` A ) e. V -> ( x e. A -> [ x ] R e. _V ) )
2	1	ralrimiv	|- ( ( R |` A ) e. V -> A. x e. A [ x ] R e. _V )
3		dfiun2g	|- ( A. x e. A [ x ] R e. _V -> U_ x e. A [ x ] R = U. { y | E. x e. A y = [ x ] R } )
4	2 3	syl	|- ( ( R |` A ) e. V -> U_ x e. A [ x ] R = U. { y | E. x e. A y = [ x ] R } )
5	4	eqcomd	|- ( ( R |` A ) e. V -> U. { y | E. x e. A y = [ x ] R } = U_ x e. A [ x ] R )
6		df-qs	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
7	6	unieqi	|- U. ( A /. R ) = U. { y | E. x e. A y = [ x ] R }
8		df-ec	|- [ x ] R = ( R " { x } )
9	8	a1i	|- ( x e. A -> [ x ] R = ( R " { x } ) )
10	9	iuneq2i	|- U_ x e. A [ x ] R = U_ x e. A ( R " { x } )
11		imaiun	|- ( R " U_ x e. A { x } ) = U_ x e. A ( R " { x } )
12		iunid	|- U_ x e. A { x } = A
13	12	imaeq2i	|- ( R " U_ x e. A { x } ) = ( R " A )
14	10 11 13	3eqtr2ri	|- ( R " A ) = U_ x e. A [ x ] R
15	5 7 14	3eqtr4g	|- ( ( R |` A ) e. V -> U. ( A /. R ) = ( R " A ) )