Theorem iuneq1 4973

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ⊆ wss 3905  ∪ ciun 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-v 3457  df-ss 3922  df-iun 4958

This theorem is referenced by:  iuneq1d  4984  iinvdif  5046  iunxprg  5062  iununi  5065  iunopeqop  5504  iunsuc  6448  funopsn  7144  funopsnOLD  7145  funiunfv  7246  onfununi  8324  iunfi  9296  ttrclselem1  9690  ttrclselem2  9691  rankuni2b  9821  pwsdompw  10182  ackbij1lem7  10204  r1om  10222  fictb  10223  cfsmolem  10249  ituniiun  10401  domtriomlem  10421  domtriom  10422  inar1  10755  fsum2d  15818  fsumiun  15869  ackbijnn  15878  fprod2d  16031  prmreclem5  16975  lpival  21492  fiuncmp  23561  ovolfiniun  25660  ovoliunnul  25666  finiunmbl  25703  volfiniun  25706  voliunlem1  25709  iuninc  32905  ofpreima2  33011  gsumpart  33383  esum2dlem  34482  sigaclfu2  34511  sigapildsyslem  34551  fiunelros  34564  bnj548  35285  bnj554  35287  bnj594  35300  neibastop2lem  36871  ttceq  36999  istotbnd3  38422  0totbnd  38424  sstotbnd2  38425  sstotbnd  38426  sstotbnd3  38427  totbndbnd  38440  prdstotbnd  38445  cntotbnd  38447  heibor  38472  dfrcl4  44402  iunrelexp0  44428  comptiunov2i  44432  corclrcl  44433  cotrcltrcl  44451  trclfvdecomr  44454  dfrtrcl4  44464  corcltrcl  44465  cotrclrcl  44468  fiiuncl  45785  sge0iunmptlemfi  47127  caragenfiiuncl  47229  carageniuncllem1  47235  ovnsubadd2lem  47359