Theorem unieq 4862

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 3981	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4861	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3982	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4861	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3940	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  unieqi  4863  unieqd  4864  uniintsn  4928  iununi  5042  treq  5200  eqsnuniex  5299  elvvuni  5702  unielrel  6233  unixp0  6242  unixpid  6243  limeq  6330  unizlim  6442  iotauni2  6465  opabiotafun  6915  uniexg  7688  onsucuni2  7779  onuninsuci  7785  orduninsuc  7788  undefval  8220  en1b  8966  nnunifi  9195  fissuni  9261  infeq5i  9551  infeq5  9552  rnttrcl  9637  ttrclselem2  9641  trcl  9643  rankuni  9781  rankxplim3  9799  iunfictbso  10030  cflim2  10179  cfss  10181  cfslb  10182  fin2i  10211  fin1a2lem10  10325  fin1a2lem11  10326  fin1a2lem12  10327  itunisuc  10335  ituniiun  10338  hsmex  10348  dominf  10361  zornn0g  10421  dominfac  10490  wununi  10623  wunex2  10655  wuncval2  10664  incexclem  15795  mrcfval  17568  mrisval  17590  acsdrsel  18503  isacs4lem  18504  isacs5lem  18505  acsdrscl  18506  isps  18528  isdir  18558  sylow2a  19588  uniopn  22875  istopon  22890  eltg3  22940  tgdom  22956  indistopon  22979  cldval  23001  ntrfval  23002  clsfval  23003  mretopd  23070  neifval  23077  lpfval  23116  isperf  23129  tgrest  23137  ist0  23298  ist1  23299  ishaus  23300  iscnrm  23301  iscmp  23366  cmpcov  23367  cmpcovf  23369  cncmp  23370  fincmp  23371  cmpsublem  23377  cmpsub  23378  tgcmp  23379  cmpcld  23380  uncmp  23381  hauscmplem  23384  cmpfi  23386  isconn  23391  is1stc  23419  2ndc1stc  23429  2ndcsep  23437  isref  23487  isptfin  23494  islocfin  23495  comppfsc  23510  kgenval  23513  1stckgenlem  23531  txcmplem1  23619  txcmplem2  23620  kqval  23704  flffval  23967  fclsval  23986  fcfval  24011  alexsublem  24022  alexsubb  24024  alexsubALTlem2  24026  alexsubALTlem3  24027  alexsubALTlem4  24028  alexsubALT  24029  ptcmplem2  24031  ptcmplem3  24032  ptcmplem5  24034  cnextval  24039  iscfilu  24265  icccmplem1  24801  icccmplem2  24802  bndth  24938  lebnumlem3  24943  om1val  25010  pi1val  25017  ovolicc2  25502  isplig  30565  hsupval  31423  acunirnmpt  32750  iscref  34007  crefi  34010  cmpcref  34013  pcmplfin  34023  sigaclcu  34280  prsiga  34294  sigaclci  34295  unelsiga  34297  sigagenval  34303  unelldsys  34321  sigapildsys  34325  ldgenpisyslem1  34326  rossros  34343  measvun  34372  ismbfm  34414  dya2iocuni  34446  oms0  34460  omssubadd  34463  carsgsigalem  34478  fiunelcarsg  34479  carsgclctunlem1  34480  carsgclctunlem2  34482  carsgclctunlem3  34483  carsgclctun  34484  pmeasmono  34487  pmeasadd  34488  fissorduni  35252  fineqvnttrclselem2  35285  wevgblacfn  35310  kur14  35417  ispconn  35424  cvmscbv  35459  cvmsi  35466  cvmsval  35467  nnuni  35928  dfrdg2  35994  brbigcup  36097  dfbigcup2  36098  fobigcup  36099  brapply  36137  dfrdg4  36152  isfne  36540  fneval  36553  fnemeet1  36567  fnemeet2  36568  fnejoin1  36569  fnejoin2  36570  tailfval  36573  ordtoplem  36636  onsucsuccmpi  36644  limsucncmpi  36646  ordcmp  36648  ttctr  36694  ttcmin  36697  dfttc2g  36707  bj-ismoore  37436  dissneqlem  37673  finxpreclem3  37726  pibp19  37747  pibp21  37748  pibt2  37750  heicant  37993  ovoliunnfl  38000  voliunnfl  38002  volsupnfl  38003  mbfresfi  38004  cover2  38053  cover2g  38054  istotbnd3  38109  sstotbnd  38113  heiborlem1  38149  heiborlem6  38154  heiborlem8  38156  dmqseqim  39079  isnacs3  43159  nacsfix  43161  onsupnmax  43677  onov0suclim  43723  pwelg  44008  mnuprdlem1  44720  mnuprdlem2  44721  mnuunid  44725  mnurndlem1  44729  ismnushort  44749  csbfv12gALTVD  45346  stoweidlem35  46484  stoweidlem39  46488  stoweidlem50  46499  stoweidlem57  46506  issal  46763  salunicl  46765  saluncl  46766  prsal  46767  salgenval  46770  intsaluni  46778  salgenn0  46780  salgencl  46781  sssalgen  46784  salgenss  46785  salgenuni  46786  issalgend  46787  dfsalgen2  46790  issalnnd  46794  meadjuni  46906  ismeannd  46916  omeunile  46954  caragenunicl  46973  isomennd  46980  issmflem  47176  termco  49971  onsetreclem1  50195