Theorem iuneq1 4950

Description: Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem iuneq1

Step	Hyp	Ref	Expression
1		iunss1 4948	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶)
2		iunss1 4948	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)
3	1, 2	anim12i 614	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶))
4		eqss 3937	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3937	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 ↔ (∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3889  ∪ ciun 4933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-v 3431  df-ss 3906  df-iun 4935

This theorem is referenced by:  iuneq1d  4961  iinvdif  5022  iunxprg  5038  iununi  5041  iunopeqop  5475  iunsuc  6410  funopsn  7101  funopsnOLD  7102  funiunfv  7203  onfununi  8281  iunfi  9253  ttrclselem1  9646  ttrclselem2  9647  rankuni2b  9777  pwsdompw  10125  ackbij1lem7  10147  r1om  10165  fictb  10166  cfsmolem  10192  ituniiun  10344  domtriomlem  10364  domtriom  10365  inar1  10698  fsum2d  15733  fsumiun  15784  ackbijnn  15793  fprod2d  15946  prmreclem5  16891  lpival  21322  fiuncmp  23369  ovolfiniun  25468  ovoliunnul  25474  finiunmbl  25511  volfiniun  25514  voliunlem1  25517  iuninc  32630  ofpreima2  32739  gsumpart  33124  esum2dlem  34236  sigaclfu2  34265  sigapildsyslem  34305  fiunelros  34318  bnj548  35039  bnj554  35041  bnj594  35054  neibastop2lem  36542  ttceq  36670  istotbnd3  38092  0totbnd  38094  sstotbnd2  38095  sstotbnd  38096  sstotbnd3  38097  totbndbnd  38110  prdstotbnd  38115  cntotbnd  38117  heibor  38142  dfrcl4  44103  iunrelexp0  44129  comptiunov2i  44133  corclrcl  44134  cotrcltrcl  44152  trclfvdecomr  44155  dfrtrcl4  44165  corcltrcl  44166  cotrclrcl  44169  fiiuncl  45496  sge0iunmptlemfi  46841  caragenfiiuncl  46943  carageniuncllem1  46949  ovnsubadd2lem  47073