Theorem iuneq2 5010

Description: Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.)

Assertion

Ref	Expression
iuneq2	⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Proof of Theorem iuneq2

Step	Hyp	Ref	Expression
1		ss2iun 5009	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)
2		ss2iun 5009	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
3	1, 2	anim12i 613	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵) → (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 ∧ ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
4		eqss 3998	. . . 4 ⊢ (𝐵 = 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵))
5	4	ralbii 3092	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵))
6		r19.26 3110	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵))
7	5, 6	bitri 275	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵))
8		eqss 3998	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 ∧ ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
9	3, 7, 8	3imtr4i 292	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ∀wral 3060   ⊆ wss 3950  ∪ ciun 4990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-v 3481  df-ss 3967  df-iun 4992

This theorem is referenced by:  iuneq2i  5012  iuneq2dv  5015  iunxdif3  5094  oa0r  8577  om0r  8578  om1r  8582  oe1m  8584  oaass  8600  oarec  8601  omass  8619  oeoalem  8635  oeoelem  8637  cardiun  10023  kmlem11  10202  iuncld  23054  comppfsc  23541  istotbnd3  37779  sstotbnd  37783  heibor  37829  iuneq12f  38171  cnvtrclfv  43742  iuneq2df  45057