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∈AB∈D→∀x∈AB∈C↔y|∃x∈Ay=B⊆C

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢y=z→y=B↔z=B
2 1 rexbidv ⊢y=z→∃x∈Ay=B↔∃x∈Az=B
3 2 cbvabv ⊢y|∃x∈Ay=B=z|∃x∈Az=B
4 3 sseq1i ⊢y|∃x∈Ay=B⊆C↔z|∃x∈Az=B⊆C
5 r19.23v ⊢∀x∈Az=B→z∈C↔∃x∈Az=B→z∈C
6 5 albii ⊢∀z∀x∈Az=B→z∈C↔∀z∃x∈Az=B→z∈C
7 ralcom4 ⊢∀x∈A∀zz=B→z∈C↔∀z∀x∈Az=B→z∈C
8 abss ⊢z|∃x∈Az=B⊆C↔∀z∃x∈Az=B→z∈C
9 6 7 8 3bitr4i ⊢∀x∈A∀zz=B→z∈C↔z|∃x∈Az=B⊆C
10 4 9 bitr4i ⊢y|∃x∈Ay=B⊆C↔∀x∈A∀zz=B→z∈C
11 nfv ⊢ℲzB∈C
12 eleq1 ⊢z=B→z∈C↔B∈C
13 11 12 ceqsalg ⊢B∈D→∀zz=B→z∈C↔B∈C
14 13 ralimi ⊢∀x∈AB∈D→∀x∈A∀zz=B→z∈C↔B∈C
15 ralbi ⊢∀x∈A∀zz=B→z∈C↔B∈C→∀x∈A∀zz=B→z∈C↔∀x∈AB∈C
16 14 15 syl ⊢∀x∈AB∈D→∀x∈A∀zz=B→z∈C↔∀x∈AB∈C
17 10 16 bitr2id ⊢∀x∈AB∈D→∀x∈AB∈C↔y|∃x∈Ay=B⊆C