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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-v 3453  df-ss 3916  df-iun 4953

This theorem is used by:  iuneq1d  4979  iinvdif  5040  iunxprg  5056  iununi  5059  iunopeqop  5494  iunsuc  6449  funopsn  7149  funopsnOLD  7150  funiunfv  7250  onfununi  8342  iunfi  9325  ttrclselem1  9719  ttrclselem2  9720  rankuni2b  9860  pwsdompw  10274  ackbij1lem7  10296  hfom  10314  fictb  10315  cfsmolem  10341  ituniiun  10493  domtriomlem  10513  domtriom  10514  inar1  10853  fsum2d  15930  fsumiun  15981  ackbijnn  15990  fprod2d  16141  prmreclem5  17091  lpival  21641  fiuncmp  23715  ovolfiniun  25815  ovoliunnul  25821  finiunmbl  25858  volfiniun  25861  voliunlem1  25864  iuninc  33148  ofpreima2  33253  gsumpart  33617  esum2dlem  34717  sigaclfu2  34746  sigapildsyslem  34787  fiunelros  34800  bnj548  35520  bnj554  35522  bnj594  35535  neibastop2lem  37128  ttceq  37256  istotbnd3  38685  0totbnd  38687  sstotbnd2  38688  sstotbnd  38689  sstotbnd3  38690  totbndbnd  38703  prdstotbnd  38708  cntotbnd  38710  heibor  38735  dfrcl4  44661  iunrelexp0  44687  comptiunov2i  44691  corclrcl  44692  cotrcltrcl  44710  trclfvdecomr  44713  dfrtrcl4  44723  corcltrcl  44724  cotrclrcl  44727  fiiuncl  46051  sge0iunmptlemfi  47392  caragenfiiuncl  47494  carageniuncllem1  47500  ovnsubadd2lem  47624