Theorem iuneq1 4977

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ⊆ wss 3913  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-v 3465  df-ss 3930  df-iun 4962

This theorem is referenced by:  iuneq1d  4988  iinvdif  5050  iunxprg  5066  iununi  5069  iunopeqop  5505  iunsuc  6449  funopsn  7145  funopsnOLD  7146  funiunfv  7247  onfununi  8327  iunfi  9299  ttrclselem1  9693  ttrclselem2  9694  rankuni2b  9824  pwsdompw  10185  ackbij1lem7  10207  r1om  10225  fictb  10226  cfsmolem  10253  ituniiun  10405  domtriomlem  10425  domtriom  10426  inar1  10759  fsum2d  15821  fsumiun  15872  ackbijnn  15881  fprod2d  16034  prmreclem5  16979  lpival  21460  fiuncmp  23529  ovolfiniun  25628  ovoliunnul  25634  finiunmbl  25671  volfiniun  25674  voliunlem1  25677  iuninc  32845  ofpreima2  32951  gsumpart  33323  esum2dlem  34426  sigaclfu2  34455  sigapildsyslem  34495  fiunelros  34508  bnj548  35229  bnj554  35231  bnj594  35244  neibastop2lem  36759  ttceq  36887  istotbnd3  38309  0totbnd  38311  sstotbnd2  38312  sstotbnd  38313  sstotbnd3  38314  totbndbnd  38327  prdstotbnd  38332  cntotbnd  38334  heibor  38359  dfrcl4  44293  iunrelexp0  44319  comptiunov2i  44323  corclrcl  44324  cotrcltrcl  44342  trclfvdecomr  44345  dfrtrcl4  44355  corcltrcl  44356  cotrclrcl  44359  fiiuncl  45676  sge0iunmptlemfi  47018  caragenfiiuncl  47120  carageniuncllem1  47126  ovnsubadd2lem  47250