Theorem iuneq1 4951

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3890  ∪ ciun 4934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3432  df-ss 3907  df-iun 4936

This theorem is referenced by:  iuneq1d  4962  iinvdif  5023  iunxprg  5039  iununi  5042  iunsuc  6405  funopsn  7096  funiunfv  7197  onfununi  8275  iunfi  9247  ttrclselem1  9640  ttrclselem2  9641  rankuni2b  9771  pwsdompw  10119  ackbij1lem7  10141  r1om  10159  fictb  10160  cfsmolem  10186  ituniiun  10338  domtriomlem  10358  domtriom  10359  inar1  10692  fsum2d  15727  fsumiun  15778  ackbijnn  15787  fprod2d  15940  prmreclem5  16885  lpival  21317  fiuncmp  23382  ovolfiniun  25481  ovoliunnul  25487  finiunmbl  25524  volfiniun  25527  voliunlem1  25530  iuninc  32648  ofpreima2  32757  gsumpart  33142  esum2dlem  34255  sigaclfu2  34284  sigapildsyslem  34324  fiunelros  34337  bnj548  35058  bnj554  35060  bnj594  35073  neibastop2lem  36561  ttceq  36689  istotbnd3  38109  0totbnd  38111  sstotbnd2  38112  sstotbnd  38113  sstotbnd3  38114  totbndbnd  38127  prdstotbnd  38132  cntotbnd  38134  heibor  38159  dfrcl4  44124  iunrelexp0  44150  comptiunov2i  44154  corclrcl  44155  cotrcltrcl  44173  trclfvdecomr  44176  dfrtrcl4  44186  corcltrcl  44187  cotrclrcl  44190  fiiuncl  45517  sge0iunmptlemfi  46862  caragenfiiuncl  46964  carageniuncllem1  46970  ovnsubadd2lem  47094