Theorem unieq 4920

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 4041	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4919	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 4042	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4919	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 4000	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

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

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 3956  df-ss 3966  df-uni 4910

This theorem is referenced by:  unieqi  4922  unieqd  4923  uniintsn  4992  iununi  5103  treq  5274  eqsnuniex  5360  elvvuni  5753  unielrel  6274  unixp0  6283  unixpid  6284  limeq  6377  unizlim  6488  iotauni2  6513  opabiotafun  6973  uniexg  7730  onsucuni2  7822  onuninsuci  7829  orduninsuc  7832  undefval  8261  en1b  9023  en1bOLD  9024  nnunifi  9294  fissuni  9357  infeq5i  9631  infeq5  9632  rnttrcl  9717  ttrclselem2  9721  trcl  9723  rankuni  9858  rankxplim3  9876  iunfictbso  10109  cflim2  10258  cfss  10260  cfslb  10261  fin2i  10290  fin1a2lem10  10404  fin1a2lem11  10405  fin1a2lem12  10406  itunisuc  10414  ituniiun  10417  hsmex  10427  dominf  10440  zornn0g  10500  dominfac  10568  wununi  10701  wunex2  10733  wuncval2  10742  incexclem  15782  mrcfval  17552  mrisval  17574  acsdrsel  18496  isacs4lem  18497  isacs5lem  18498  acsdrscl  18499  isps  18521  isdir  18551  sylow2a  19487  uniopn  22399  istopon  22414  eltg3  22465  tgdom  22481  indistopon  22504  cldval  22527  ntrfval  22528  clsfval  22529  mretopd  22596  neifval  22603  lpfval  22642  isperf  22655  tgrest  22663  ist0  22824  ist1  22825  ishaus  22826  iscnrm  22827  iscmp  22892  cmpcov  22893  cmpcovf  22895  cncmp  22896  fincmp  22897  cmpsublem  22903  cmpsub  22904  tgcmp  22905  cmpcld  22906  uncmp  22907  hauscmplem  22910  cmpfi  22912  isconn  22917  is1stc  22945  2ndc1stc  22955  2ndcsep  22963  isref  23013  isptfin  23020  islocfin  23021  comppfsc  23036  kgenval  23039  1stckgenlem  23057  txcmplem1  23145  txcmplem2  23146  kqval  23230  flffval  23493  fclsval  23512  fcfval  23537  alexsublem  23548  alexsubb  23550  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  ptcmplem2  23557  ptcmplem3  23558  ptcmplem5  23560  cnextval  23565  iscfilu  23793  icccmplem1  24338  icccmplem2  24339  bndth  24474  lebnumlem3  24479  om1val  24546  pi1val  24553  ovolicc2  25039  isplig  29729  hsupval  30587  acunirnmpt  31884  iscref  32824  crefi  32827  cmpcref  32830  pcmplfin  32840  sigaclcu  33115  prsiga  33129  sigaclci  33130  unelsiga  33132  sigagenval  33138  unelldsys  33156  sigapildsys  33160  ldgenpisyslem1  33161  rossros  33178  measvun  33207  ismbfm  33249  dya2iocuni  33282  oms0  33296  omssubadd  33299  carsgsigalem  33314  fiunelcarsg  33315  carsgclctunlem1  33316  carsgclctunlem2  33318  carsgclctunlem3  33319  carsgclctun  33320  pmeasmono  33323  pmeasadd  33324  kur14  34207  ispconn  34214  cvmscbv  34249  cvmsi  34256  cvmsval  34257  nnuni  34696  dfrdg2  34767  brbigcup  34870  dfbigcup2  34871  fobigcup  34872  brapply  34910  dfrdg4  34923  isfne  35224  fneval  35237  fnemeet1  35251  fnemeet2  35252  fnejoin1  35253  fnejoin2  35254  tailfval  35257  ordtoplem  35320  onsucsuccmpi  35328  limsucncmpi  35330  ordcmp  35332  bj-ismoore  35986  dissneqlem  36221  finxpreclem3  36274  pibp19  36295  pibp21  36296  pibt2  36298  heicant  36523  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  mbfresfi  36534  cover2  36583  cover2g  36584  istotbnd3  36639  sstotbnd  36643  heiborlem1  36679  heiborlem6  36684  heiborlem8  36686  dmqseqim  37526  isnacs3  41448  nacsfix  41450  onsupnmax  41977  onov0suclim  42024  pwelg  42311  mnuprdlem1  43031  mnuprdlem2  43032  mnuunid  43036  mnurndlem1  43040  ismnushort  43060  csbfv12gALTVD  43660  stoweidlem35  44751  stoweidlem39  44755  stoweidlem50  44766  stoweidlem57  44773  issal  45030  salunicl  45032  saluncl  45033  prsal  45034  salgenval  45037  intsaluni  45045  salgenn0  45047  salgencl  45048  sssalgen  45051  salgenss  45052  salgenuni  45053  issalgend  45054  dfsalgen2  45057  issalnnd  45061  meadjuni  45173  ismeannd  45183  omeunile  45221  caragenunicl  45240  isomennd  45247  issmflem  45443  onsetreclem1  47750