This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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