Theorem iuneq1 4937

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ⊆ wss 3938  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-v 3498  df-in 3945  df-ss 3954  df-iun 4923

This theorem is referenced by:  iuneq1d  4948  iinvdif  5004  iunxprg  5020  iununi  5023  iunsuc  6275  funopsn  6912  funiunfv  7009  onfununi  7980  iunfi  8814  rankuni2b  9284  pwsdompw  9628  ackbij1lem7  9650  r1om  9668  fictb  9669  cfsmolem  9694  ituniiun  9846  domtriomlem  9866  domtriom  9867  inar1  10199  fsum2d  15128  fsumiun  15178  ackbijnn  15185  fprod2d  15337  prmreclem5  16258  lpival  20020  fiuncmp  22014  ovolfiniun  24104  ovoliunnul  24110  finiunmbl  24147  volfiniun  24150  voliunlem1  24153  iuninc  30314  ofpreima2  30413  esum2dlem  31353  sigaclfu2  31382  sigapildsyslem  31422  fiunelros  31435  bnj548  32171  bnj554  32173  bnj594  32186  trpredlem1  33068  trpredtr  33071  trpredmintr  33072  trpredrec  33079  neibastop2lem  33710  istotbnd3  35051  0totbnd  35053  sstotbnd2  35054  sstotbnd  35055  sstotbnd3  35056  totbndbnd  35069  prdstotbnd  35074  cntotbnd  35076  heibor  35101  dfrcl4  40028  iunrelexp0  40054  comptiunov2i  40058  corclrcl  40059  cotrcltrcl  40077  trclfvdecomr  40080  dfrtrcl4  40090  corcltrcl  40091  cotrclrcl  40094  fiiuncl  41334  iuneq1i  41357  sge0iunmptlemfi  42702  caragenfiiuncl  42804  carageniuncllem1  42810  ovnsubadd2lem  42934