Theorem iuneq1 4686

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ⊆ wss 3715  ∪ ciun 4672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-v 3342  df-in 3722  df-ss 3729  df-iun 4674

This theorem is referenced by:  iuneq1d  4697  iinvdif  4744  iunxprg  4759  iununi  4762  iunsuc  5968  funopsn  6576  funiunfv  6669  onfununi  7607  iunfi  8419  rankuni2b  8889  pwsdompw  9218  ackbij1lem7  9240  r1om  9258  fictb  9259  cfsmolem  9284  ituniiun  9436  domtriomlem  9456  domtriom  9457  inar1  9789  fsum2d  14701  fsumiun  14752  ackbijnn  14759  fprod2d  14910  prmreclem5  15826  lpival  19447  fiuncmp  21409  ovolfiniun  23469  ovoliunnul  23475  finiunmbl  23512  volfiniun  23515  voliunlem1  23518  iuninc  29686  ofpreima2  29775  esum2dlem  30463  sigaclfu2  30493  sigapildsyslem  30533  fiunelros  30546  bnj548  31274  bnj554  31276  bnj594  31289  trpredlem1  32032  trpredtr  32035  trpredmintr  32036  trpredrec  32043  neibastop2lem  32661  istotbnd3  33883  0totbnd  33885  sstotbnd2  33886  sstotbnd  33887  sstotbnd3  33888  totbndbnd  33901  prdstotbnd  33906  cntotbnd  33908  heibor  33933  dfrcl4  38470  iunrelexp0  38496  comptiunov2i  38500  corclrcl  38501  cotrcltrcl  38519  trclfvdecomr  38522  dfrtrcl4  38532  corcltrcl  38533  cotrclrcl  38536  fiiuncl  39733  iuneq1i  39758  sge0iunmptlemfi  41133  caragenfiiuncl  41235  carageniuncllem1  41241  ovnsubadd2lem  41365