Metamath Proof Explorer


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 ) )