Theorem iuneq1 5014

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ⊆ wss 3949  ∪ ciun 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-v 3477  df-in 3956  df-ss 3966  df-iun 5000

This theorem is referenced by:  iuneq1d  5025  iinvdif  5084  iunxprg  5100  iununi  5103  iunsuc  6450  funopsn  7146  funiunfv  7247  onfununi  8341  iunfi  9340  ttrclselem1  9720  ttrclselem2  9721  rankuni2b  9848  pwsdompw  10199  ackbij1lem7  10221  r1om  10239  fictb  10240  cfsmolem  10265  ituniiun  10417  domtriomlem  10437  domtriom  10438  inar1  10770  fsum2d  15717  fsumiun  15767  ackbijnn  15774  fprod2d  15925  prmreclem5  16853  lpival  20883  fiuncmp  22908  ovolfiniun  25018  ovoliunnul  25024  finiunmbl  25061  volfiniun  25064  voliunlem1  25067  iuninc  31792  ofpreima2  31891  gsumpart  32207  esum2dlem  33090  sigaclfu2  33119  sigapildsyslem  33159  fiunelros  33172  bnj548  33908  bnj554  33910  bnj594  33923  neibastop2lem  35245  istotbnd3  36639  0totbnd  36641  sstotbnd2  36642  sstotbnd  36643  sstotbnd3  36644  totbndbnd  36657  prdstotbnd  36662  cntotbnd  36664  heibor  36689  dfrcl4  42427  iunrelexp0  42453  comptiunov2i  42457  corclrcl  42458  cotrcltrcl  42476  trclfvdecomr  42479  dfrtrcl4  42489  corcltrcl  42490  cotrclrcl  42493  fiiuncl  43752  iuneq1i  43774  sge0iunmptlemfi  45129  caragenfiiuncl  45231  carageniuncllem1  45237  ovnsubadd2lem  45361