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  31823  ofpreima2  31922  gsumpart  32238  esum2dlem  33121  sigaclfu2  33150  sigapildsyslem  33190  fiunelros  33203  bnj548  33939  bnj554  33941  bnj594  33954  neibastop2lem  35293  istotbnd3  36687  0totbnd  36689  sstotbnd2  36690  sstotbnd  36691  sstotbnd3  36692  totbndbnd  36705  prdstotbnd  36710  cntotbnd  36712  heibor  36737  dfrcl4  42475  iunrelexp0  42501  comptiunov2i  42505  corclrcl  42506  cotrcltrcl  42524  trclfvdecomr  42527  dfrtrcl4  42537  corcltrcl  42538  cotrclrcl  42541  fiiuncl  43800  iuneq1i  43822  sge0iunmptlemfi  45177  caragenfiiuncl  45279  carageniuncllem1  45285  ovnsubadd2lem  45409