Theorem iuneq1 4920

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ⊆ wss 3866  ∪ ciun 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-v 3410  df-in 3873  df-ss 3883  df-iun 4906

This theorem is referenced by:  iuneq1d  4931  iinvdif  4988  iunxprg  5004  iununi  5007  iunsuc  6295  funopsn  6963  funiunfv  7061  onfununi  8078  iunfi  8964  trpredlem1  9332  trpredtr  9335  trpredmintr  9336  trpredrec  9342  rankuni2b  9469  pwsdompw  9818  ackbij1lem7  9840  r1om  9858  fictb  9859  cfsmolem  9884  ituniiun  10036  domtriomlem  10056  domtriom  10057  inar1  10389  fsum2d  15335  fsumiun  15385  ackbijnn  15392  fprod2d  15543  prmreclem5  16473  lpival  20283  fiuncmp  22301  ovolfiniun  24398  ovoliunnul  24404  finiunmbl  24441  volfiniun  24444  voliunlem1  24447  iuninc  30619  ofpreima2  30723  gsumpart  31034  esum2dlem  31772  sigaclfu2  31801  sigapildsyslem  31841  fiunelros  31854  bnj548  32590  bnj554  32592  bnj594  32605  neibastop2lem  34286  istotbnd3  35666  0totbnd  35668  sstotbnd2  35669  sstotbnd  35670  sstotbnd3  35671  totbndbnd  35684  prdstotbnd  35689  cntotbnd  35691  heibor  35716  dfrcl4  40961  iunrelexp0  40987  comptiunov2i  40991  corclrcl  40992  cotrcltrcl  41010  trclfvdecomr  41013  dfrtrcl4  41023  corcltrcl  41024  cotrclrcl  41027  fiiuncl  42286  iuneq1i  42308  sge0iunmptlemfi  43626  caragenfiiuncl  43728  carageniuncllem1  43734  ovnsubadd2lem  43858