Theorem iuneq1 4938

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ⊆ wss 3883  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rex 3064  df-v 3433  df-ss 3900  df-iun 4923

This theorem is referenced by:  iuneq1d  4949  iinvdif  5009  iunxprg  5025  iununi  5028  iunopeqop  5462  iunsuc  6397  funopsn  7090  funopsnOLD  7091  funiunfv  7192  onfununi  8271  iunfi  9243  ttrclselem1  9637  ttrclselem2  9638  rankuni2b  9768  pwsdompw  10116  ackbij1lem7  10138  r1om  10156  fictb  10157  cfsmolem  10183  ituniiun  10335  domtriomlem  10355  domtriom  10356  inar1  10689  fsum2d  15724  fsumiun  15775  ackbijnn  15784  fprod2d  15937  prmreclem5  16882  lpival  21317  fiuncmp  23387  ovolfiniun  25486  ovoliunnul  25492  finiunmbl  25529  volfiniun  25532  voliunlem1  25535  iuninc  32649  ofpreima2  32758  gsumpart  33144  esum2dlem  34276  sigaclfu2  34305  sigapildsyslem  34345  fiunelros  34358  bnj548  35079  bnj554  35081  bnj594  35094  neibastop2lem  36588  ttceq  36716  istotbnd3  38138  0totbnd  38140  sstotbnd2  38141  sstotbnd  38142  sstotbnd3  38143  totbndbnd  38156  prdstotbnd  38161  cntotbnd  38163  heibor  38188  dfrcl4  44120  iunrelexp0  44146  comptiunov2i  44150  corclrcl  44151  cotrcltrcl  44169  trclfvdecomr  44172  dfrtrcl4  44182  corcltrcl  44183  cotrclrcl  44186  fiiuncl  45513  sge0iunmptlemfi  46856  caragenfiiuncl  46958  carageniuncllem1  46964  ovnsubadd2lem  47088