Theorem unieq 4811

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

Syntax hints:   → wi 4   = wceq 1538  ∪ cuni 4800

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801

This theorem is referenced by:  unieqi  4813  unieqd  4814  uniintsn  4875  iununi  4984  treq  5142  elvvuni  5592  unielrel  6093  unixp0  6102  unixpid  6103  limeq  6171  unizlim  6275  opabiotafun  6719  uniexg  7446  onsucuni2  7529  onuninsuci  7535  orduninsuc  7538  undefval  7925  en1b  8560  nnunifi  8753  fissuni  8813  infeq5i  9083  infeq5  9084  trcl  9154  rankuni  9276  rankxplim3  9294  iunfictbso  9525  cflim2  9674  cfss  9676  cfslb  9677  fin2i  9706  fin1a2lem10  9820  fin1a2lem11  9821  fin1a2lem12  9822  itunisuc  9830  ituniiun  9833  hsmex  9843  dominf  9856  zornn0g  9916  dominfac  9984  wununi  10117  wunex2  10149  wuncval2  10158  incexclem  15183  mrcfval  16871  mrisval  16893  acsdrsel  17769  isacs4lem  17770  isacs5lem  17771  acsdrscl  17772  isps  17804  isdir  17834  sylow2a  18736  uniopn  21502  istopon  21517  eltg3  21567  tgdom  21583  indistopon  21606  cldval  21628  ntrfval  21629  clsfval  21630  mretopd  21697  neifval  21704  lpfval  21743  isperf  21756  tgrest  21764  ist0  21925  ist1  21926  ishaus  21927  iscnrm  21928  iscmp  21993  cmpcov  21994  cmpcovf  21996  cncmp  21997  fincmp  21998  cmpsublem  22004  cmpsub  22005  tgcmp  22006  cmpcld  22007  uncmp  22008  hauscmplem  22011  cmpfi  22013  isconn  22018  is1stc  22046  2ndc1stc  22056  2ndcsep  22064  isref  22114  isptfin  22121  islocfin  22122  comppfsc  22137  kgenval  22140  1stckgenlem  22158  txcmplem1  22246  txcmplem2  22247  kqval  22331  flffval  22594  fclsval  22613  fcfval  22638  alexsublem  22649  alexsubb  22651  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  alexsubALT  22656  ptcmplem2  22658  ptcmplem3  22659  ptcmplem5  22661  cnextval  22666  iscfilu  22894  icccmplem1  23427  icccmplem2  23428  bndth  23563  lebnumlem3  23568  om1val  23635  pi1val  23642  ovolicc2  24126  isplig  28259  hsupval  29117  acunirnmpt  30422  iscref  31197  crefi  31200  cmpcref  31203  pcmplfin  31213  sigaclcu  31486  prsiga  31500  sigaclci  31501  unelsiga  31503  sigagenval  31509  unelldsys  31527  sigapildsys  31531  ldgenpisyslem1  31532  rossros  31549  measvun  31578  ismbfm  31620  isanmbfm  31624  dya2iocuni  31651  oms0  31665  omssubadd  31668  carsgsigalem  31683  fiunelcarsg  31684  carsgclctunlem1  31685  carsgclctunlem2  31687  carsgclctunlem3  31688  carsgclctun  31689  pmeasmono  31692  pmeasadd  31693  kur14  32576  ispconn  32583  cvmscbv  32618  cvmsi  32625  cvmsval  32626  dfrdg2  33153  brbigcup  33472  dfbigcup2  33473  fobigcup  33474  brapply  33512  dfrdg4  33525  isfne  33800  fneval  33813  fnemeet1  33827  fnemeet2  33828  fnejoin1  33829  fnejoin2  33830  tailfval  33833  ordtoplem  33896  onsucsuccmpi  33904  limsucncmpi  33906  ordcmp  33908  bj-ismoore  34520  dissneqlem  34757  finxpreclem3  34810  pibp19  34831  pibp21  34832  pibt2  34834  heicant  35092  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  mbfresfi  35103  cover2  35152  cover2g  35153  istotbnd3  35209  sstotbnd  35213  heiborlem1  35249  heiborlem6  35254  heiborlem8  35256  dmqseqim  36050  isnacs3  39651  nacsfix  39653  pwelg  40259  mnuprdlem1  40980  mnuprdlem2  40981  mnuunid  40985  mnurndlem1  40989  csbfv12gALTVD  41605  stoweidlem35  42677  stoweidlem39  42681  stoweidlem50  42692  stoweidlem57  42699  issal  42956  salunicl  42958  saluncl  42959  prsal  42960  salgenval  42963  intsaluni  42969  salgenn0  42971  salgencl  42972  sssalgen  42975  salgenss  42976  salgenuni  42977  issalgend  42978  dfsalgen2  42981  issalnnd  42985  meadjuni  43096  ismeannd  43106  omeunile  43144  caragenunicl  43163  isomennd  43170  issmflem  43361  onsetreclem1  45234