Theorem iuneq1 4966

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ⊆ wss 3904  ∪ ciun 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3087  df-v 3456  df-ss 3921  df-iun 4951

This theorem is referenced by:  iuneq1d  4977  iinvdif  5037  iunxprg  5053  iununi  5056  iunopeqop  5490  iunsuc  6433  funopsn  7130  funopsnOLD  7131  funiunfv  7232  onfununi  8312  iunfi  9286  ttrclselem1  9680  ttrclselem2  9681  rankuni2b  9811  pwsdompw  10159  ackbij1lem7  10181  r1om  10199  fictb  10200  cfsmolem  10227  ituniiun  10379  domtriomlem  10399  domtriom  10400  inar1  10733  fsum2d  15798  fsumiun  15849  ackbijnn  15858  fprod2d  16011  prmreclem5  16956  lpival  21391  fiuncmp  23461  ovolfiniun  25560  ovoliunnul  25566  finiunmbl  25603  volfiniun  25606  voliunlem1  25609  iuninc  32757  ofpreima2  32865  gsumpart  33240  esum2dlem  34386  sigaclfu2  34415  sigapildsyslem  34455  fiunelros  34468  bnj548  35189  bnj554  35191  bnj594  35204  neibastop2lem  36717  ttceq  36845  istotbnd3  38267  0totbnd  38269  sstotbnd2  38270  sstotbnd  38271  sstotbnd3  38272  totbndbnd  38285  prdstotbnd  38290  cntotbnd  38292  heibor  38317  dfrcl4  44249  iunrelexp0  44275  comptiunov2i  44279  corclrcl  44280  cotrcltrcl  44298  trclfvdecomr  44301  dfrtrcl4  44311  corcltrcl  44312  cotrclrcl  44315  fiiuncl  45642  sge0iunmptlemfi  46984  caragenfiiuncl  47086  carageniuncllem1  47092  ovnsubadd2lem  47216