Theorem iuneq1 4500

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ⊆ wss 3555  ∪ ciun 4485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-v 3188  df-in 3562  df-ss 3569  df-iun 4487

This theorem is referenced by:  iuneq1d  4511  iinvdif  4558  iunxprg  4573  iununi  4576  iunsuc  5766  funopsn  6367  funiunfv  6460  onfununi  7383  iunfi  8198  rankuni2b  8660  pwsdompw  8970  ackbij1lem7  8992  r1om  9010  fictb  9011  cfsmolem  9036  ituniiun  9188  domtriomlem  9208  domtriom  9209  inar1  9541  fsum2d  14430  fsumiun  14480  ackbijnn  14485  fprod2d  14636  prmreclem5  15548  lpival  19164  fiuncmp  21117  ovolfiniun  23176  ovoliunnul  23182  finiunmbl  23219  volfiniun  23222  voliunlem1  23225  iuninc  29221  ofpreima2  29306  esum2dlem  29932  sigaclfu2  29962  sigapildsyslem  30002  fiunelros  30015  bnj548  30672  bnj554  30674  bnj594  30687  trpredlem1  31425  trpredtr  31428  trpredmintr  31429  trpredrec  31436  neibastop2lem  31994  istotbnd3  33199  0totbnd  33201  sstotbnd2  33202  sstotbnd  33203  sstotbnd3  33204  totbndbnd  33217  prdstotbnd  33222  cntotbnd  33224  heibor  33249  dfrcl4  37446  iunrelexp0  37472  comptiunov2i  37476  corclrcl  37477  cotrcltrcl  37495  trclfvdecomr  37498  dfrtrcl4  37508  corcltrcl  37509  cotrclrcl  37512  fiiuncl  38716  iuneq1i  38741  sge0iunmptlemfi  39934  caragenfiiuncl  40033  carageniuncllem1  40039  ovnsubadd2lem  40163