Theorem uniiunlem 2135

Description: A subset relationship useful for converting union to indexed union using dfiun2 2591 or dfiun2g 2590 and intersection to indexed intersection using dfiin2 2592.

Assertion

Ref	Expression
uniiunlem	⊢ (∀x ∈ A B ∈ D → (∀x ∈ A B ∈ C ↔ {y∣∃x ∈ A y = B} ⊆ C))

Distinct variable groups:   y,A   y,B   x,C   x,y

Proof of Theorem uniiunlem

Step	Hyp	Ref	Expression
1		hbra1 1690	. . . . 5 ⊢ (∀x ∈ A B ∈ C → ∀x∀x ∈ A B ∈ C)
2		ax-17 973	. . . . 5 ⊢ (z ∈ C → ∀x z ∈ C)
3		ra4 1697	. . . . . 6 ⊢ (∀x ∈ A B ∈ C → (x ∈ A → B ∈ C))
4		eleq1a 1546	. . . . . 6 ⊢ (B ∈ C → (z = B → z ∈ C))
5	3, 4	syl6 22	. . . . 5 ⊢ (∀x ∈ A B ∈ C → (x ∈ A → (z = B → z ∈ C)))
6	1, 2, 5	r19.23ad 1748	. . . 4 ⊢ (∀x ∈ A B ∈ C → (∃x ∈ A z = B → z ∈ C))
7	6	19.21aiv 1288	. . 3 ⊢ (∀x ∈ A B ∈ C → ∀z(∃x ∈ A z = B → z ∈ C))
8		hbre1 1692	. . . . . . 7 ⊢ (∃x ∈ A z = B → ∀x∃x ∈ A z = B)
9	8, 2	hbim 1009	. . . . . 6 ⊢ ((∃x ∈ A z = B → z ∈ C) → ∀x(∃x ∈ A z = B → z ∈ C))
10	9	hbal 1007	. . . . 5 ⊢ (∀z(∃x ∈ A z = B → z ∈ C) → ∀x∀z(∃x ∈ A z = B → z ∈ C))
11		csbeq1a 2009	. . . . . . . . . . . 12 ⊢ (x = w → B = [w / x]B)
12	11	eqcoms 1481	. . . . . . . . . . 11 ⊢ (w = x → B = [w / x]B)
13	12	eqcomd 1483	. . . . . . . . . 10 ⊢ (w = x → [w / x]B = B)
14	13	eqeq1d 1486	. . . . . . . . 9 ⊢ (w = x → ([w / x]B = B ↔ B = B))
15		eqid 1478	. . . . . . . . 9 ⊢ B = B
16	14, 15	a4eiv 1276	. . . . . . . 8 ⊢ ∃w[w / x]B = B
17		visset 1816	. . . . . . . . . . . . . . . . . 18 ⊢ w ∈ V
18		ax-17 973	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ w → ∀x z ∈ w)
19	17, 18	hbcsb1 2028	. . . . . . . . . . . . . . . . 17 ⊢ (z ∈ [w / x]B → ∀x z ∈ [w / x]B)
20	19	hbeleq 1570	. . . . . . . . . . . . . . . 16 ⊢ (z = [w / x]B → ∀x z = [w / x]B)
21		eqeq1 1484	. . . . . . . . . . . . . . . 16 ⊢ (z = [w / x]B → (z = B ↔ [w / x]B = B))
22	20, 21	rexbid 1665	. . . . . . . . . . . . . . 15 ⊢ (z = [w / x]B → (∃x ∈ A z = B ↔ ∃x ∈ A [w / x]B = B))
23		eleq1 1537	. . . . . . . . . . . . . . 15 ⊢ (z = [w / x]B → (z ∈ C ↔ [w / x]B ∈ C))
24	22, 23	imbi12d 628	. . . . . . . . . . . . . 14 ⊢ (z = [w / x]B → ((∃x ∈ A z = B → z ∈ C) ↔ (∃x ∈ A [w / x]B = B → [w / x]B ∈ C)))
25	24	cla4gv 1865	. . . . . . . . . . . . 13 ⊢ ([w / x]B ∈ D → (∀z(∃x ∈ A z = B → z ∈ C) → (∃x ∈ A [w / x]B = B → [w / x]B ∈ C)))
26		ra4e 1698	. . . . . . . . . . . . 13 ⊢ ((x ∈ A ⋀ [w / x]B = B) → ∃x ∈ A [w / x]B = B)
27	25, 26	syl7 23	. . . . . . . . . . . 12 ⊢ ([w / x]B ∈ D → (∀z(∃x ∈ A z = B → z ∈ C) → ((x ∈ A ⋀ [w / x]B = B) → [w / x]B ∈ C)))
28	27	exp4a 380	. . . . . . . . . . 11 ⊢ ([w / x]B ∈ D → (∀z(∃x ∈ A z = B → z ∈ C) → (x ∈ A → ([w / x]B = B → [w / x]B ∈ C))))
29	28	com4r 41	. . . . . . . . . 10 ⊢ ([w / x]B = B → ([w / x]B ∈ D → (∀z(∃x ∈ A z = B → z ∈ C) → (x ∈ A → [w / x]B ∈ C))))
30		eleq1 1537	. . . . . . . . . 10 ⊢ ([w / x]B = B → ([w / x]B ∈ D ↔ B ∈ D))
31		eleq1 1537	. . . . . . . . . . . 12 ⊢ ([w / x]B = B → ([w / x]B ∈ C ↔ B ∈ C))
32	31	imbi2d 614	. . . . . . . . . . 11 ⊢ ([w / x]B = B → ((x ∈ A → [w / x]B ∈ C) ↔ (x ∈ A → B ∈ C)))
33	32	imbi2d 614	. . . . . . . . . 10 ⊢ ([w / x]B = B → ((∀z(∃x ∈ A z = B → z ∈ C) → (x ∈ A → [w / x]B ∈ C)) ↔ (∀z(∃x ∈ A z = B → z ∈ C) → (x ∈ A → B ∈ C))))
34	29, 30, 33	3imtr3d 544	. . . . . . . . 9 ⊢ ([w / x]B = B → (B ∈ D → (∀z(∃x ∈ A z = B → z ∈ C) → (x ∈ A → B ∈ C))))
35	34	19.23aiv 1297	. . . . . . . 8 ⊢ (∃w[w / x]B = B → (B ∈ D → (∀z(∃x ∈ A z = B → z ∈ C) → (x ∈ A → B ∈ C))))
36	16, 35	ax-mp 7	. . . . . . 7 ⊢ (B ∈ D → (∀z(∃x ∈ A z = B → z ∈ C) → (x ∈ A → B ∈ C)))
37	36	imp3a 361	. . . . . 6 ⊢ (B ∈ D → ((∀z(∃x ∈ A z = B → z ∈ C) ⋀ x ∈ A) → B ∈ C))
38	37	com12 11	. . . . 5 ⊢ ((∀z(∃x ∈ A z = B → z ∈ C) ⋀ x ∈ A) → (B ∈ D → B ∈ C))
39	10, 38	r19.20da 1711	. . . 4 ⊢ (∀z(∃x ∈ A z = B → z ∈ C) → (∀x ∈ A B ∈ D → ∀x ∈ A B ∈ C))
40	39	com12 11	. . 3 ⊢ (∀x ∈ A B ∈ D → (∀z(∃x ∈ A z = B → z ∈ C) → ∀x ∈ A B ∈ C))
41	7, 40	impbid2 520	. 2 ⊢ (∀x ∈ A B ∈ D → (∀x ∈ A B ∈ C ↔ ∀z(∃x ∈ A z = B → z ∈ C)))
42		abss 2120	. . 3 ⊢ ({z∣∃x ∈ A z = B} ⊆ C ↔ ∀z(∃x ∈ A z = B → z ∈ C))
43		eqeq1 1484	. . . . . 6 ⊢ (z = y → (z = B ↔ y = B))
44	43	rexbidv 1667	. . . . 5 ⊢ (z = y → (∃x ∈ A z = B ↔ ∃x ∈ A y = B))
45	44	cbvabv 1912	. . . 4 ⊢ {z∣∃x ∈ A z = B} = {y∣∃x ∈ A y = B}
46	45	sseq1i 2088	. . 3 ⊢ ({z∣∃x ∈ A z = B} ⊆ C ↔ {y∣∃x ∈ A y = B} ⊆ C)
47	42, 46	bitr3 175	. 2 ⊢ (∀z(∃x ∈ A z = B → z ∈ C) ↔ {y∣∃x ∈ A y = B} ⊆ C)
48	41, 47	syl6bb 538	1 ⊢ (∀x ∈ A B ∈ D → (∀x ∈ A B ∈ C ↔ {y∣∃x ∈ A y = B} ⊆ C))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 956   = wceq 958   ∈ wcel 960  ∃wex 982  {cab 1466  ∀wral 1648  ∃wrex 1649  [csb 2004   ⊆ wss 2050

This theorem is referenced by:  iunopnt 7600

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-rex 1653  df-v 1815  df-sbc 1945  df-csb 2005  df-in 2054  df-ss 2056

Copyright terms: Public domain