Theorem iuneq1 4975

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3906  ∪ ciun 4958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-v 3459  df-ss 3923  df-iun 4960

This theorem is used by:  iuneq1d  4986  iinvdif  5048  iunxprg  5064  iununi  5067  iunopeqop  5506  iunsuc  6452  funopsn  7150  funopsnOLD  7151  funiunfv  7251  onfununi  8334  iunfi  9307  ttrclselem1  9701  ttrclselem2  9702  rankuni2b  9832  pwsdompw  10202  ackbij1lem7  10224  r1om  10242  fictb  10243  cfsmolem  10269  ituniiun  10421  domtriomlem  10441  domtriom  10442  inar1  10775  fsum2d  15845  fsumiun  15896  ackbijnn  15905  fprod2d  16058  prmreclem5  17002  lpival  21542  fiuncmp  23611  ovolfiniun  25711  ovoliunnul  25717  finiunmbl  25754  volfiniun  25757  voliunlem1  25760  iuninc  32976  ofpreima2  33082  gsumpart  33447  esum2dlem  34546  sigaclfu2  34575  sigapildsyslem  34616  fiunelros  34629  bnj548  35350  bnj554  35352  bnj594  35365  neibastop2lem  36928  ttceq  37056  istotbnd3  38480  0totbnd  38482  sstotbnd2  38483  sstotbnd  38484  sstotbnd3  38485  totbndbnd  38498  prdstotbnd  38503  cntotbnd  38505  heibor  38530  dfrcl4  44460  iunrelexp0  44486  comptiunov2i  44490  corclrcl  44491  cotrcltrcl  44509  trclfvdecomr  44512  dfrtrcl4  44522  corcltrcl  44523  cotrclrcl  44526  fiiuncl  45843  sge0iunmptlemfi  47185  caragenfiiuncl  47287  carageniuncllem1  47293  ovnsubadd2lem  47417