Theorem iuneq1 4534

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ⊆ wss 3574  ∪ ciun 4520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-iun 4522

This theorem is referenced by:  iuneq1d  4545  iinvdif  4592  iunxprg  4607  iununi  4610  iunsuc  5807  funopsn  6413  funiunfv  6506  onfununi  7438  iunfi  8254  rankuni2b  8716  pwsdompw  9026  ackbij1lem7  9048  r1om  9066  fictb  9067  cfsmolem  9092  ituniiun  9244  domtriomlem  9264  domtriom  9265  inar1  9597  fsum2d  14502  fsumiun  14553  ackbijnn  14560  fprod2d  14711  prmreclem5  15624  lpival  19245  fiuncmp  21207  ovolfiniun  23269  ovoliunnul  23275  finiunmbl  23312  volfiniun  23315  voliunlem1  23318  iuninc  29379  ofpreima2  29466  esum2dlem  30154  sigaclfu2  30184  sigapildsyslem  30224  fiunelros  30237  bnj548  30967  bnj554  30969  bnj594  30982  trpredlem1  31727  trpredtr  31730  trpredmintr  31731  trpredrec  31738  neibastop2lem  32355  istotbnd3  33570  0totbnd  33572  sstotbnd2  33573  sstotbnd  33574  sstotbnd3  33575  totbndbnd  33588  prdstotbnd  33593  cntotbnd  33595  heibor  33620  dfrcl4  37968  iunrelexp0  37994  comptiunov2i  37998  corclrcl  37999  cotrcltrcl  38017  trclfvdecomr  38020  dfrtrcl4  38030  corcltrcl  38031  cotrclrcl  38034  fiiuncl  39234  iuneq1i  39259  sge0iunmptlemfi  40630  caragenfiiuncl  40729  carageniuncllem1  40735  ovnsubadd2lem  40859