Theorem unieq 4918

Description: Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by BJ, 13-Apr-2024.)

Assertion

Ref	Expression
unieq	⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Proof of Theorem unieq

Step	Hyp	Ref	Expression
1		eqimss 4039	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4917	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 4040	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4917	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3998	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1542  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3954  df-ss 3964  df-uni 4908

This theorem is referenced by:  unieqi  4920  unieqd  4921  uniintsn  4990  iununi  5101  treq  5272  eqsnuniex  5358  elvvuni  5750  unielrel  6270  unixp0  6279  unixpid  6280  limeq  6373  unizlim  6484  iotauni2  6509  opabiotafun  6968  uniexg  7725  onsucuni2  7817  onuninsuci  7824  orduninsuc  7827  undefval  8256  en1b  9019  en1bOLD  9020  nnunifi  9290  fissuni  9353  infeq5i  9627  infeq5  9628  rnttrcl  9713  ttrclselem2  9717  trcl  9719  rankuni  9854  rankxplim3  9872  iunfictbso  10105  cflim2  10254  cfss  10256  cfslb  10257  fin2i  10286  fin1a2lem10  10400  fin1a2lem11  10401  fin1a2lem12  10402  itunisuc  10410  ituniiun  10413  hsmex  10423  dominf  10436  zornn0g  10496  dominfac  10564  wununi  10697  wunex2  10729  wuncval2  10738  incexclem  15778  mrcfval  17548  mrisval  17570  acsdrsel  18492  isacs4lem  18493  isacs5lem  18494  acsdrscl  18495  isps  18517  isdir  18547  sylow2a  19480  uniopn  22381  istopon  22396  eltg3  22447  tgdom  22463  indistopon  22486  cldval  22509  ntrfval  22510  clsfval  22511  mretopd  22578  neifval  22585  lpfval  22624  isperf  22637  tgrest  22645  ist0  22806  ist1  22807  ishaus  22808  iscnrm  22809  iscmp  22874  cmpcov  22875  cmpcovf  22877  cncmp  22878  fincmp  22879  cmpsublem  22885  cmpsub  22886  tgcmp  22887  cmpcld  22888  uncmp  22889  hauscmplem  22892  cmpfi  22894  isconn  22899  is1stc  22927  2ndc1stc  22937  2ndcsep  22945  isref  22995  isptfin  23002  islocfin  23003  comppfsc  23018  kgenval  23021  1stckgenlem  23039  txcmplem1  23127  txcmplem2  23128  kqval  23212  flffval  23475  fclsval  23494  fcfval  23519  alexsublem  23530  alexsubb  23532  alexsubALTlem2  23534  alexsubALTlem3  23535  alexsubALTlem4  23536  alexsubALT  23537  ptcmplem2  23539  ptcmplem3  23540  ptcmplem5  23542  cnextval  23547  iscfilu  23775  icccmplem1  24320  icccmplem2  24321  bndth  24456  lebnumlem3  24461  om1val  24528  pi1val  24535  ovolicc2  25021  isplig  29707  hsupval  30565  acunirnmpt  31862  iscref  32762  crefi  32765  cmpcref  32768  pcmplfin  32778  sigaclcu  33053  prsiga  33067  sigaclci  33068  unelsiga  33070  sigagenval  33076  unelldsys  33094  sigapildsys  33098  ldgenpisyslem1  33099  rossros  33116  measvun  33145  ismbfm  33187  dya2iocuni  33220  oms0  33234  omssubadd  33237  carsgsigalem  33252  fiunelcarsg  33253  carsgclctunlem1  33254  carsgclctunlem2  33256  carsgclctunlem3  33257  carsgclctun  33258  pmeasmono  33261  pmeasadd  33262  kur14  34145  ispconn  34152  cvmscbv  34187  cvmsi  34194  cvmsval  34195  nnuni  34634  dfrdg2  34705  brbigcup  34808  dfbigcup2  34809  fobigcup  34810  brapply  34848  dfrdg4  34861  isfne  35162  fneval  35175  fnemeet1  35189  fnemeet2  35190  fnejoin1  35191  fnejoin2  35192  tailfval  35195  ordtoplem  35258  onsucsuccmpi  35266  limsucncmpi  35268  ordcmp  35270  bj-ismoore  35924  dissneqlem  36159  finxpreclem3  36212  pibp19  36233  pibp21  36234  pibt2  36236  heicant  36461  ovoliunnfl  36468  voliunnfl  36470  volsupnfl  36471  mbfresfi  36472  cover2  36521  cover2g  36522  istotbnd3  36577  sstotbnd  36581  heiborlem1  36617  heiborlem6  36622  heiborlem8  36624  dmqseqim  37464  isnacs3  41381  nacsfix  41383  onsupnmax  41910  onov0suclim  41957  pwelg  42244  mnuprdlem1  42964  mnuprdlem2  42965  mnuunid  42969  mnurndlem1  42973  ismnushort  42993  csbfv12gALTVD  43593  stoweidlem35  44686  stoweidlem39  44690  stoweidlem50  44701  stoweidlem57  44708  issal  44965  salunicl  44967  saluncl  44968  prsal  44969  salgenval  44972  intsaluni  44980  salgenn0  44982  salgencl  44983  sssalgen  44986  salgenss  44987  salgenuni  44988  issalgend  44989  dfsalgen2  44992  issalnnd  44996  meadjuni  45108  ismeannd  45118  omeunile  45156  caragenunicl  45175  isomennd  45182  issmflem  45378  onsetreclem1  47652