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