Theorem uniiunlem

Description: A subset relationship useful for converting union to indexed union using dfiun2 or dfiun2g and intersection to indexed intersection using dfiin2 . (Contributed by NM, 5-Oct-2006) (Proof shortened by Mario Carneiro, 26-Sep-2015)

	Ref	Expression
Assertion	uniiunlem	|- ( A. x e. A B e. D -> ( A. x e. A B e. C <-> { y | E. x e. A y = B } C_ C ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	|- ( y = z -> ( y = B <-> z = B ) )
2	1	rexbidv	|- ( y = z -> ( E. x e. A y = B <-> E. x e. A z = B ) )
3	2	cbvabv	|- { y | E. x e. A y = B } = { z | E. x e. A z = B }
4	3	sseq1i	|- ( { y | E. x e. A y = B } C_ C <-> { z | E. x e. A z = B } C_ C )
5		r19.23v	|- ( A. x e. A ( z = B -> z e. C ) <-> ( E. x e. A z = B -> z e. C ) )
6	5	albii	|- ( A. z A. x e. A ( z = B -> z e. C ) <-> A. z ( E. x e. A z = B -> z e. C ) )
7		ralcom4	|- ( A. x e. A A. z ( z = B -> z e. C ) <-> A. z A. x e. A ( z = B -> z e. C ) )
8		abss	|- ( { z | E. x e. A z = B } C_ C <-> A. z ( E. x e. A z = B -> z e. C ) )
9	6 7 8	3bitr4i	|- ( A. x e. A A. z ( z = B -> z e. C ) <-> { z | E. x e. A z = B } C_ C )
10	4 9	bitr4i	|- ( { y | E. x e. A y = B } C_ C <-> A. x e. A A. z ( z = B -> z e. C ) )
11		nfv	|- F/ z B e. C
12		eleq1	|- ( z = B -> ( z e. C <-> B e. C ) )
13	11 12	ceqsalg	|- ( B e. D -> ( A. z ( z = B -> z e. C ) <-> B e. C ) )
14	13	ralimi	|- ( A. x e. A B e. D -> A. x e. A ( A. z ( z = B -> z e. C ) <-> B e. C ) )
15		ralbi	|- ( A. x e. A ( A. z ( z = B -> z e. C ) <-> B e. C ) -> ( A. x e. A A. z ( z = B -> z e. C ) <-> A. x e. A B e. C ) )
16	14 15	syl	|- ( A. x e. A B e. D -> ( A. x e. A A. z ( z = B -> z e. C ) <-> A. x e. A B e. C ) )
17	10 16	bitr2id	|- ( A. x e. A B e. D -> ( A. x e. A B e. C <-> { y | E. x e. A y = B } C_ C ) )