Theorem iuneq1 4963

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 4961	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶)
2		iunss1 4961	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)
3	1, 2	anim12i 613	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶))
4		eqss 3949	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3949	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 ↔ (∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3901  ∪ ciun 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-v 3442  df-ss 3918  df-iun 4948

This theorem is referenced by:  iuneq1d  4974  iinvdif  5035  iunxprg  5051  iununi  5054  iunsuc  6404  funopsn  7093  funiunfv  7194  onfununi  8273  iunfi  9243  ttrclselem1  9634  ttrclselem2  9635  rankuni2b  9765  pwsdompw  10113  ackbij1lem7  10135  r1om  10153  fictb  10154  cfsmolem  10180  ituniiun  10332  domtriomlem  10352  domtriom  10353  inar1  10686  fsum2d  15694  fsumiun  15744  ackbijnn  15751  fprod2d  15904  prmreclem5  16848  lpival  21279  fiuncmp  23348  ovolfiniun  25458  ovoliunnul  25464  finiunmbl  25501  volfiniun  25504  voliunlem1  25507  iuninc  32635  ofpreima2  32744  gsumpart  33146  esum2dlem  34249  sigaclfu2  34278  sigapildsyslem  34318  fiunelros  34331  bnj548  35053  bnj554  35055  bnj594  35068  neibastop2lem  36554  istotbnd3  37972  0totbnd  37974  sstotbnd2  37975  sstotbnd  37976  sstotbnd3  37977  totbndbnd  37990  prdstotbnd  37995  cntotbnd  37997  heibor  38022  dfrcl4  43917  iunrelexp0  43943  comptiunov2i  43947  corclrcl  43948  cotrcltrcl  43966  trclfvdecomr  43969  dfrtrcl4  43979  corcltrcl  43980  cotrclrcl  43983  fiiuncl  45310  sge0iunmptlemfi  46657  caragenfiiuncl  46759  carageniuncllem1  46765  ovnsubadd2lem  46889