Theorem unieq 4849

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 3973	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4848	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3974	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4848	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3932	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1547  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-uni 4839

This theorem is referenced by:  unieqi  4850  unieqd  4851  uniintsn  4915  iununi  5028  treq  5186  eqsnuniex  5290  elvvuni  5695  unielrel  6225  unixp0  6234  unixpid  6235  limeq  6322  unizlim  6434  iotauni2  6457  opabiotafun  6907  uniexg  7683  onsucuni2  7774  onuninsuci  7780  orduninsuc  7783  undefval  8216  en1b  8962  nnunifi  9191  fissuni  9257  infeq5i  9548  infeq5  9549  rnttrcl  9634  ttrclselem2  9638  trcl  9640  rankuni  9778  rankxplim3  9796  iunfictbso  10027  cflim2  10176  cfss  10178  cfslb  10179  fin2i  10208  fin1a2lem10  10322  fin1a2lem11  10323  fin1a2lem12  10324  itunisuc  10332  ituniiun  10335  hsmex  10345  dominf  10358  zornn0g  10418  dominfac  10487  wununi  10620  wunex2  10652  wuncval2  10661  incexclem  15792  mrcfval  17565  mrisval  17587  acsdrsel  18500  isacs4lem  18501  isacs5lem  18502  acsdrscl  18503  isps  18525  isdir  18555  sylow2a  19585  uniopn  22880  istopon  22895  eltg3  22945  tgdom  22961  indistopon  22984  cldval  23006  ntrfval  23007  clsfval  23008  mretopd  23075  neifval  23082  lpfval  23121  isperf  23134  tgrest  23142  ist0  23303  ist1  23304  ishaus  23305  iscnrm  23306  iscmp  23371  cmpcov  23372  cmpcovf  23374  cncmp  23375  fincmp  23376  cmpsublem  23382  cmpsub  23383  tgcmp  23384  cmpcld  23385  uncmp  23386  hauscmplem  23389  cmpfi  23391  isconn  23396  is1stc  23424  2ndc1stc  23434  2ndcsep  23442  isref  23492  isptfin  23499  islocfin  23500  comppfsc  23515  kgenval  23518  1stckgenlem  23536  txcmplem1  23624  txcmplem2  23625  kqval  23709  flffval  23972  fclsval  23991  fcfval  24016  alexsublem  24027  alexsubb  24029  alexsubALTlem2  24031  alexsubALTlem3  24032  alexsubALTlem4  24033  alexsubALT  24034  ptcmplem2  24036  ptcmplem3  24037  ptcmplem5  24039  cnextval  24044  iscfilu  24270  icccmplem1  24806  icccmplem2  24807  bndth  24943  lebnumlem3  24948  om1val  25015  pi1val  25022  ovolicc2  25507  isplig  30565  hsupval  31423  acunirnmpt  32751  iscref  34028  crefi  34031  cmpcref  34034  pcmplfin  34044  sigaclcu  34301  prsiga  34315  sigaclci  34316  unelsiga  34318  sigagenval  34324  unelldsys  34342  sigapildsys  34346  ldgenpisyslem1  34347  rossros  34364  measvun  34393  ismbfm  34435  dya2iocuni  34467  oms0  34481  omssubadd  34484  carsgsigalem  34499  fiunelcarsg  34500  carsgclctunlem1  34501  carsgclctunlem2  34503  carsgclctunlem3  34504  carsgclctun  34505  pmeasmono  34508  pmeasadd  34509  fissorduni  35271  fineqvnttrclselem2  35303  wevgblacfn  35337  kur14  35444  ispconn  35451  cvmscbv  35486  cvmsi  35493  cvmsval  35494  nnuni  35955  dfrdg2  36021  brbigcup  36124  dfbigcup2  36125  fobigcup  36126  brapply  36164  dfrdg4  36179  isfne  36567  fneval  36580  fnemeet1  36594  fnemeet2  36595  fnejoin1  36596  fnejoin2  36597  tailfval  36600  ordtoplem  36663  onsucsuccmpi  36671  limsucncmpi  36673  ordcmp  36675  ttctr  36721  ttcmin  36724  dfttc2g  36734  bj-ismoore  37463  dissneqlem  37702  finxpreclem3  37755  pibp19  37776  pibp21  37777  pibt2  37779  heicant  38022  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  mbfresfi  38033  cover2  38082  cover2g  38083  istotbnd3  38138  sstotbnd  38142  heiborlem1  38178  heiborlem6  38183  heiborlem8  38185  dmqseqim  39108  isnacs3  43159  nacsfix  43161  onsupnmax  43673  onov0suclim  43719  pwelg  44004  mnuprdlem1  44716  mnuprdlem2  44717  mnuunid  44721  mnurndlem1  44725  ismnushort  44745  csbfv12gALTVD  45342  stoweidlem35  46478  stoweidlem39  46482  stoweidlem50  46493  stoweidlem57  46500  issal  46757  salunicl  46759  saluncl  46760  prsal  46761  salgenval  46764  intsaluni  46772  salgenn0  46774  salgencl  46775  sssalgen  46778  salgenss  46779  salgenuni  46780  issalgend  46781  dfsalgen2  46784  issalnnd  46788  meadjuni  46900  ismeannd  46910  omeunile  46948  caragenunicl  46967  isomennd  46974  issmflem  47170  termco  49971  onsetreclem1  50195