Theorem iuneq2 5016

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 5015	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)
2		ss2iun 5015	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
3	1, 2	anim12i 613	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵) → (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 ∧ ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
4		eqss 4011	. . . 4 ⊢ (𝐵 = 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵))
5	4	ralbii 3091	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵))
6		r19.26 3109	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵))
7	5, 6	bitri 275	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 ↔ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵))
8		eqss 4011	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 ∧ ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
9	3, 7, 8	3imtr4i 292	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ∀wral 3059   ⊆ wss 3963  ∪ ciun 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-v 3480  df-ss 3980  df-iun 4998

This theorem is referenced by:  iuneq2i  5018  iuneq2dv  5021  iunxdif3  5100  oa0r  8575  om0r  8576  om1r  8580  oe1m  8582  oaass  8598  oarec  8599  omass  8617  oeoalem  8633  oeoelem  8635  cardiun  10020  kmlem11  10199  iuncld  23069  comppfsc  23556  istotbnd3  37758  sstotbnd  37762  heibor  37808  iuneq12f  38150  cnvtrclfv  43714  iuneq2df  44986