Theorem iuneq1 5008

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3951  ∪ ciun 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-v 3482  df-ss 3968  df-iun 4993

This theorem is referenced by:  iuneq1d  5019  iinvdif  5080  iunxprg  5096  iununi  5099  iunsuc  6469  funopsn  7168  funiunfv  7268  onfununi  8381  iunfi  9383  ttrclselem1  9765  ttrclselem2  9766  rankuni2b  9893  pwsdompw  10243  ackbij1lem7  10265  r1om  10283  fictb  10284  cfsmolem  10310  ituniiun  10462  domtriomlem  10482  domtriom  10483  inar1  10815  fsum2d  15807  fsumiun  15857  ackbijnn  15864  fprod2d  16017  prmreclem5  16958  lpival  21334  fiuncmp  23412  ovolfiniun  25536  ovoliunnul  25542  finiunmbl  25579  volfiniun  25582  voliunlem1  25585  iuninc  32573  ofpreima2  32676  gsumpart  33060  esum2dlem  34093  sigaclfu2  34122  sigapildsyslem  34162  fiunelros  34175  bnj548  34911  bnj554  34913  bnj594  34926  neibastop2lem  36361  istotbnd3  37778  0totbnd  37780  sstotbnd2  37781  sstotbnd  37782  sstotbnd3  37783  totbndbnd  37796  prdstotbnd  37801  cntotbnd  37803  heibor  37828  dfrcl4  43689  iunrelexp0  43715  comptiunov2i  43719  corclrcl  43720  cotrcltrcl  43738  trclfvdecomr  43741  dfrtrcl4  43751  corcltrcl  43752  cotrclrcl  43755  fiiuncl  45070  sge0iunmptlemfi  46428  caragenfiiuncl  46530  carageniuncllem1  46536  ovnsubadd2lem  46660