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 x A B D x A B C y | x A y = B C

Proof

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