Theorem unieq 4942

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 4067	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4941	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 4068	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4941	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 4026	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932

This theorem is referenced by:  unieqi  4943  unieqd  4944  uniintsn  5009  iununi  5122  treq  5291  eqsnuniex  5379  elvvuni  5776  unielrel  6305  unixp0  6314  unixpid  6315  limeq  6407  unizlim  6518  iotauni2  6542  opabiotafun  7002  uniexg  7775  onsucuni2  7870  onuninsuci  7877  orduninsuc  7880  undefval  8317  en1b  9088  en1bOLD  9089  nnunifi  9355  fissuni  9427  infeq5i  9705  infeq5  9706  rnttrcl  9791  ttrclselem2  9795  trcl  9797  rankuni  9932  rankxplim3  9950  iunfictbso  10183  cflim2  10332  cfss  10334  cfslb  10335  fin2i  10364  fin1a2lem10  10478  fin1a2lem11  10479  fin1a2lem12  10480  itunisuc  10488  ituniiun  10491  hsmex  10501  dominf  10514  zornn0g  10574  dominfac  10642  wununi  10775  wunex2  10807  wuncval2  10816  incexclem  15884  mrcfval  17666  mrisval  17688  acsdrsel  18613  isacs4lem  18614  isacs5lem  18615  acsdrscl  18616  isps  18638  isdir  18668  sylow2a  19661  uniopn  22924  istopon  22939  eltg3  22990  tgdom  23006  indistopon  23029  cldval  23052  ntrfval  23053  clsfval  23054  mretopd  23121  neifval  23128  lpfval  23167  isperf  23180  tgrest  23188  ist0  23349  ist1  23350  ishaus  23351  iscnrm  23352  iscmp  23417  cmpcov  23418  cmpcovf  23420  cncmp  23421  fincmp  23422  cmpsublem  23428  cmpsub  23429  tgcmp  23430  cmpcld  23431  uncmp  23432  hauscmplem  23435  cmpfi  23437  isconn  23442  is1stc  23470  2ndc1stc  23480  2ndcsep  23488  isref  23538  isptfin  23545  islocfin  23546  comppfsc  23561  kgenval  23564  1stckgenlem  23582  txcmplem1  23670  txcmplem2  23671  kqval  23755  flffval  24018  fclsval  24037  fcfval  24062  alexsublem  24073  alexsubb  24075  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  ptcmplem2  24082  ptcmplem3  24083  ptcmplem5  24085  cnextval  24090  iscfilu  24318  icccmplem1  24863  icccmplem2  24864  bndth  25009  lebnumlem3  25014  om1val  25082  pi1val  25089  ovolicc2  25576  isplig  30508  hsupval  31366  acunirnmpt  32677  iscref  33790  crefi  33793  cmpcref  33796  pcmplfin  33806  sigaclcu  34081  prsiga  34095  sigaclci  34096  unelsiga  34098  sigagenval  34104  unelldsys  34122  sigapildsys  34126  ldgenpisyslem1  34127  rossros  34144  measvun  34173  ismbfm  34215  dya2iocuni  34248  oms0  34262  omssubadd  34265  carsgsigalem  34280  fiunelcarsg  34281  carsgclctunlem1  34282  carsgclctunlem2  34284  carsgclctunlem3  34285  carsgclctun  34286  pmeasmono  34289  pmeasadd  34290  wevgblacfn  35076  kur14  35184  ispconn  35191  cvmscbv  35226  cvmsi  35233  cvmsval  35234  nnuni  35689  dfrdg2  35759  brbigcup  35862  dfbigcup2  35863  fobigcup  35864  brapply  35902  dfrdg4  35915  isfne  36305  fneval  36318  fnemeet1  36332  fnemeet2  36333  fnejoin1  36334  fnejoin2  36335  tailfval  36338  ordtoplem  36401  onsucsuccmpi  36409  limsucncmpi  36411  ordcmp  36413  bj-ismoore  37071  dissneqlem  37306  finxpreclem3  37359  pibp19  37380  pibp21  37381  pibt2  37383  heicant  37615  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  mbfresfi  37626  cover2  37675  cover2g  37676  istotbnd3  37731  sstotbnd  37735  heiborlem1  37771  heiborlem6  37776  heiborlem8  37778  dmqseqim  38612  isnacs3  42666  nacsfix  42668  onsupnmax  43189  onov0suclim  43236  pwelg  43522  mnuprdlem1  44241  mnuprdlem2  44242  mnuunid  44246  mnurndlem1  44250  ismnushort  44270  csbfv12gALTVD  44870  stoweidlem35  45956  stoweidlem39  45960  stoweidlem50  45971  stoweidlem57  45978  issal  46235  salunicl  46237  saluncl  46238  prsal  46239  salgenval  46242  intsaluni  46250  salgenn0  46252  salgencl  46253  sssalgen  46256  salgenss  46257  salgenuni  46258  issalgend  46259  dfsalgen2  46262  issalnnd  46266  meadjuni  46378  ismeannd  46388  omeunile  46426  caragenunicl  46445  isomennd  46452  issmflem  46648  onsetreclem1  48797