Theorem iuneq1 4470

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ⊆ wss 3540  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-iun 4457

This theorem is referenced by:  iuneq1d  4481  iinvdif  4528  iunxprg  4543  iununi  4546  iunsuc  5724  funopsn  6319  funiunfv  6410  onfununi  7325  iunfi  8137  rankuni2b  8599  pwsdompw  8909  ackbij1lem7  8931  r1om  8949  fictb  8950  cfsmolem  8975  ituniiun  9127  domtriomlem  9147  domtriom  9148  inar1  9476  fsum2d  14344  fsumiun  14394  ackbijnn  14399  fprod2d  14550  prmreclem5  15462  lpival  19066  fiuncmp  21017  ovolfiniun  23076  ovoliunnul  23082  finiunmbl  23119  volfiniun  23122  voliunlem1  23125  iuninc  28761  ofpreima2  28849  esum2dlem  29481  sigaclfu2  29511  sigapildsyslem  29551  fiunelros  29564  bnj548  30221  bnj554  30223  bnj594  30236  trpredlem1  30971  trpredtr  30974  trpredmintr  30975  trpredrec  30982  neibastop2lem  31525  istotbnd3  32740  0totbnd  32742  sstotbnd2  32743  sstotbnd  32744  sstotbnd3  32745  totbndbnd  32758  prdstotbnd  32763  cntotbnd  32765  heibor  32790  dfrcl4  36987  iunrelexp0  37013  comptiunov2i  37017  corclrcl  37018  cotrcltrcl  37036  trclfvdecomr  37039  dfrtrcl4  37049  corcltrcl  37050  cotrclrcl  37053  fiiuncl  38259  iuneq1i  38286  sge0iunmptlemfi  39306  caragenfiiuncl  39405  carageniuncllem1  39411  ovnsubadd2lem  39535