Theorem iuneq1 4968

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

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

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-ss 3916  df-iun 4953

This theorem is used by:  iuneq1d  4979  iinvdif  5040  iunxprg  5056  iununi  5059  iunopeqop  5498  iunsuc  6445  funopsn  7144  funopsnOLD  7145  funiunfv  7245  onfununi  8330  iunfi  9310  ttrclselem1  9704  ttrclselem2  9705  rankuni2b  9835  pwsdompw  10205  ackbij1lem7  10227  r1om  10245  fictb  10246  cfsmolem  10272  ituniiun  10424  domtriomlem  10444  domtriom  10445  inar1  10784  fsum2d  15857  fsumiun  15908  ackbijnn  15917  fprod2d  16068  prmreclem5  17012  lpival  21555  fiuncmp  23629  ovolfiniun  25729  ovoliunnul  25735  finiunmbl  25772  volfiniun  25775  voliunlem1  25778  iuninc  33034  ofpreima2  33139  gsumpart  33503  esum2dlem  34602  sigaclfu2  34631  sigapildsyslem  34672  fiunelros  34685  bnj548  35406  bnj554  35408  bnj594  35421  neibastop2lem  36979  ttceq  37107  istotbnd3  38521  0totbnd  38523  sstotbnd2  38524  sstotbnd  38525  sstotbnd3  38526  totbndbnd  38539  prdstotbnd  38544  cntotbnd  38546  heibor  38571  dfrcl4  44516  iunrelexp0  44542  comptiunov2i  44546  corclrcl  44547  cotrcltrcl  44565  trclfvdecomr  44568  dfrtrcl4  44578  corcltrcl  44579  cotrclrcl  44582  fiiuncl  45899  sge0iunmptlemfi  47241  caragenfiiuncl  47343  carageniuncllem1  47349  ovnsubadd2lem  47473