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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-uni 4839

This theorem is referenced by:  unieqi  4851  unieqd  4852  uniintsn  4913  iununi  5021  treq  5178  elvvuni  5628  unielrel  6125  unixp0  6134  unixpid  6135  limeq  6203  unizlim  6307  opabiotafun  6744  uniexg  7466  onsucuni2  7549  onuninsuci  7555  orduninsuc  7558  undefval  7942  en1b  8577  nnunifi  8769  fissuni  8829  infeq5i  9099  infeq5  9100  trcl  9170  rankuni  9292  rankxplim3  9310  iunfictbso  9540  cflim2  9685  cfss  9687  cfslb  9688  fin2i  9717  fin1a2lem10  9831  fin1a2lem11  9832  fin1a2lem12  9833  itunisuc  9841  ituniiun  9844  hsmex  9854  dominf  9867  zornn0g  9927  dominfac  9995  wununi  10128  wunex2  10160  wuncval2  10169  incexclem  15191  mrcfval  16879  mrisval  16901  acsdrsel  17777  isacs4lem  17778  isacs5lem  17779  acsdrscl  17780  isps  17812  isdir  17842  sylow2a  18744  uniopn  21505  istopon  21520  eltg3  21570  tgdom  21586  indistopon  21609  cldval  21631  ntrfval  21632  clsfval  21633  mretopd  21700  neifval  21707  lpfval  21746  isperf  21759  tgrest  21767  ist0  21928  ist1  21929  ishaus  21930  iscnrm  21931  iscmp  21996  cmpcov  21997  cmpcovf  21999  cncmp  22000  fincmp  22001  cmpsublem  22007  cmpsub  22008  tgcmp  22009  cmpcld  22010  uncmp  22011  hauscmplem  22014  cmpfi  22016  isconn  22021  is1stc  22049  2ndc1stc  22059  2ndcsep  22067  isref  22117  isptfin  22124  islocfin  22125  comppfsc  22140  kgenval  22143  1stckgenlem  22161  txcmplem1  22249  txcmplem2  22250  kqval  22334  flffval  22597  fclsval  22616  fcfval  22641  alexsublem  22652  alexsubb  22654  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  alexsubALT  22659  ptcmplem2  22661  ptcmplem3  22662  ptcmplem5  22664  cnextval  22669  iscfilu  22897  icccmplem1  23430  icccmplem2  23431  bndth  23562  lebnumlem3  23567  om1val  23634  pi1val  23641  ovolicc2  24123  isplig  28253  hsupval  29111  acunirnmpt  30404  iscref  31108  crefi  31111  cmpcref  31114  pcmplfin  31124  sigaclcu  31376  prsiga  31390  sigaclci  31391  unelsiga  31393  sigagenval  31399  unelldsys  31417  sigapildsys  31421  ldgenpisyslem1  31422  rossros  31439  measvun  31468  ismbfm  31510  isanmbfm  31514  dya2iocuni  31541  oms0  31555  omssubadd  31558  carsgsigalem  31573  fiunelcarsg  31574  carsgclctunlem1  31575  carsgclctunlem2  31577  carsgclctunlem3  31578  carsgclctun  31579  pmeasmono  31582  pmeasadd  31583  kur14  32463  ispconn  32470  cvmscbv  32505  cvmsi  32512  cvmsval  32513  dfrdg2  33040  brbigcup  33359  dfbigcup2  33360  fobigcup  33361  brapply  33399  dfrdg4  33412  isfne  33687  fneval  33700  fnemeet1  33714  fnemeet2  33715  fnejoin1  33716  fnejoin2  33717  tailfval  33720  ordtoplem  33783  onsucsuccmpi  33791  limsucncmpi  33793  ordcmp  33795  bj-ismoore  34400  dissneqlem  34624  finxpreclem3  34677  pibp19  34698  pibp21  34699  pibt2  34701  heicant  34942  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  mbfresfi  34953  cover2  35004  cover2g  35005  istotbnd3  35064  sstotbnd  35068  heiborlem1  35104  heiborlem6  35109  heiborlem8  35111  dmqseqim  35905  isnacs3  39327  nacsfix  39329  pwelg  39939  mnuprdlem1  40628  mnuprdlem2  40629  mnuunid  40633  mnurndlem1  40637  csbfv12gALTVD  41253  stoweidlem35  42340  stoweidlem39  42344  stoweidlem50  42355  stoweidlem57  42362  issal  42619  salunicl  42621  saluncl  42622  prsal  42623  salgenval  42626  intsaluni  42632  salgenn0  42634  salgencl  42635  sssalgen  42638  salgenss  42639  salgenuni  42640  issalgend  42641  dfsalgen2  42644  issalnnd  42648  meadjuni  42759  ismeannd  42769  omeunile  42807  caragenunicl  42826  isomennd  42833  issmflem  43024  onsetreclem1  44827