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 ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 𝐵 ↔ 𝑧 = 𝐵 ) )
2 1 rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
3 2 cbvabv ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 }
4 3 sseq1i ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐶 ↔ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ⊆ 𝐶 )
5 r19.23v ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) )
6 5 albii ⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) )
7 ralcom4 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) ↔ ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) )
8 abss ⊢ ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ⊆ 𝐶 ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) )
9 6 7 8 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) ↔ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ⊆ 𝐶 )
10 4 9 bitr4i ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) )
11 nfv ⊢ Ⅎ 𝑧 𝐵 ∈ 𝐶
12 eleq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
13 11 12 ceqsalg ⊢ ( 𝐵 ∈ 𝐷 → ( ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) ↔ 𝐵 ∈ 𝐶 ) )
14 13 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 → ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) ↔ 𝐵 ∈ 𝐶 ) )
15 ralbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) ↔ 𝐵 ∈ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) )
16 14 15 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑧 ∈ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) )
17 10 16 bitr2id ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐶 ) )