Metamath Proof Explorer

Theorem ss2iundv

Description: Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020)

Ref Expression
Hypotheses ss2iundv.el 
|- ( ( ph /\ x e. A ) -> Y e. C )
ss2iundv.sub 
|- ( ( ph /\ x e. A /\ y = Y ) -> D = G )
ss2iundv.ss 
|- ( ( ph /\ x e. A ) -> B C_ G )
Assertion ss2iundv 
|- ( ph -> U_ x e. A B C_ U_ y e. C D )

Proof

Step Hyp Ref Expression
1 ss2iundv.el 
 |-  ( ( ph /\ x e. A ) -> Y e. C )
2 ss2iundv.sub 
 |-  ( ( ph /\ x e. A /\ y = Y ) -> D = G )
3 ss2iundv.ss 
 |-  ( ( ph /\ x e. A ) -> B C_ G )
4 nfv 
 |-  F/ x ph
5 nfv 
 |-  F/ y ph
6 nfcv 
 |-  F/_ y Y
7 nfcv 
 |-  F/_ y A
8 nfcv 
 |-  F/_ y B
9 nfcv 
 |-  F/_ x C
10 nfcv 
 |-  F/_ y C
11 nfcv 
 |-  F/_ x D
12 nfcv 
 |-  F/_ y G
13 4 5 6 7 8 9 10 11 12 1 2 3 ss2iundf 
 |-  ( ph -> U_ x e. A B C_ U_ y e. C D )