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