Theorem unieq 4812

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 3950	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	unissd 4811	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3		eqimss2 3951	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	unissd 4811	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐵 ⊆ ∪ 𝐴)
5	2, 4	eqssd 3911	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

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

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 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-uni 4802

This theorem is referenced by:  unieqi  4814  unieqd  4815  uniintsn  4880  iununi  4990  treq  5148  elvvuni  5602  unielrel  6108  unixp0  6117  unixpid  6118  limeq  6186  unizlim  6291  opabiotafun  6738  uniexg  7470  onsucuni2  7554  onuninsuci  7560  orduninsuc  7563  undefval  7958  en1b  8609  nnunifi  8815  fissuni  8875  infeq5i  9145  infeq5  9146  trcl  9216  rankuni  9338  rankxplim3  9356  iunfictbso  9587  cflim2  9736  cfss  9738  cfslb  9739  fin2i  9768  fin1a2lem10  9882  fin1a2lem11  9883  fin1a2lem12  9884  itunisuc  9892  ituniiun  9895  hsmex  9905  dominf  9918  zornn0g  9978  dominfac  10046  wununi  10179  wunex2  10211  wuncval2  10220  incexclem  15252  mrcfval  16950  mrisval  16972  acsdrsel  17856  isacs4lem  17857  isacs5lem  17858  acsdrscl  17859  isps  17891  isdir  17921  sylow2a  18824  uniopn  21610  istopon  21625  eltg3  21675  tgdom  21691  indistopon  21714  cldval  21736  ntrfval  21737  clsfval  21738  mretopd  21805  neifval  21812  lpfval  21851  isperf  21864  tgrest  21872  ist0  22033  ist1  22034  ishaus  22035  iscnrm  22036  iscmp  22101  cmpcov  22102  cmpcovf  22104  cncmp  22105  fincmp  22106  cmpsublem  22112  cmpsub  22113  tgcmp  22114  cmpcld  22115  uncmp  22116  hauscmplem  22119  cmpfi  22121  isconn  22126  is1stc  22154  2ndc1stc  22164  2ndcsep  22172  isref  22222  isptfin  22229  islocfin  22230  comppfsc  22245  kgenval  22248  1stckgenlem  22266  txcmplem1  22354  txcmplem2  22355  kqval  22439  flffval  22702  fclsval  22721  fcfval  22746  alexsublem  22757  alexsubb  22759  alexsubALTlem2  22761  alexsubALTlem3  22762  alexsubALTlem4  22763  alexsubALT  22764  ptcmplem2  22766  ptcmplem3  22767  ptcmplem5  22769  cnextval  22774  iscfilu  23002  icccmplem1  23536  icccmplem2  23537  bndth  23672  lebnumlem3  23677  om1val  23744  pi1val  23751  ovolicc2  24235  isplig  28371  hsupval  29229  acunirnmpt  30532  iscref  31327  crefi  31330  cmpcref  31333  pcmplfin  31343  sigaclcu  31616  prsiga  31630  sigaclci  31631  unelsiga  31633  sigagenval  31639  unelldsys  31657  sigapildsys  31661  ldgenpisyslem1  31662  rossros  31679  measvun  31708  ismbfm  31750  isanmbfm  31754  dya2iocuni  31781  oms0  31795  omssubadd  31798  carsgsigalem  31813  fiunelcarsg  31814  carsgclctunlem1  31815  carsgclctunlem2  31817  carsgclctunlem3  31818  carsgclctun  31819  pmeasmono  31822  pmeasadd  31823  kur14  32706  ispconn  32713  cvmscbv  32748  cvmsi  32755  cvmsval  32756  dfrdg2  33299  brbigcup  33783  dfbigcup2  33784  fobigcup  33785  brapply  33823  dfrdg4  33836  isfne  34111  fneval  34124  fnemeet1  34138  fnemeet2  34139  fnejoin1  34140  fnejoin2  34141  tailfval  34144  ordtoplem  34207  onsucsuccmpi  34215  limsucncmpi  34217  ordcmp  34219  bj-ismoore  34834  dissneqlem  35071  finxpreclem3  35124  pibp19  35145  pibp21  35146  pibt2  35148  heicant  35406  ovoliunnfl  35413  voliunnfl  35415  volsupnfl  35416  mbfresfi  35417  cover2  35466  cover2g  35467  istotbnd3  35523  sstotbnd  35527  heiborlem1  35563  heiborlem6  35568  heiborlem8  35570  dmqseqim  36364  isnacs3  40059  nacsfix  40061  pwelg  40667  mnuprdlem1  41388  mnuprdlem2  41389  mnuunid  41393  mnurndlem1  41397  csbfv12gALTVD  42013  stoweidlem35  43078  stoweidlem39  43082  stoweidlem50  43093  stoweidlem57  43100  issal  43357  salunicl  43359  saluncl  43360  prsal  43361  salgenval  43364  intsaluni  43370  salgenn0  43372  salgencl  43373  sssalgen  43376  salgenss  43377  salgenuni  43378  issalgend  43379  dfsalgen2  43382  issalnnd  43386  meadjuni  43497  ismeannd  43507  omeunile  43545  caragenunicl  43564  isomennd  43571  issmflem  43762  onsetreclem1  45719