Theorem unieq 4380

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.)

Assertion

Ref	Expression
unieq	⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Proof of Theorem unieq

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rexeq 3116	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝑥))
2	1	abbidv 2728	. 2 ⊢ (𝐴 = 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝑥})
3		dfuni2 4374	. 2 ⊢ ∪ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
4		dfuni2 4374	. 2 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝑥}
5	2, 3, 4	3eqtr4g 2669	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1475  {cab 2596  ∃wrex 2897  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4373

This theorem is referenced by:  unieqi  4381  unieqd  4382  uniintsn  4449  iununi  4546  treq  4686  elvvuni  5102  unielrel  5577  unixp0  5586  unixpid  5587  limeq  5652  unizlim  5761  opabiotafun  6169  uniex  6851  uniexg  6853  onsucuni2  6926  onuninsuci  6932  orduninsuc  6935  undefval  7289  en1b  7910  nnunifi  8096  fissuni  8154  infeq5i  8416  infeq5  8417  trcl  8487  rankuni  8609  rankxplim3  8627  iunfictbso  8820  cflim2  8968  cfss  8970  cfslb  8971  fin2i  9000  fin1a2lem10  9114  fin1a2lem11  9115  fin1a2lem12  9116  itunisuc  9124  ituniiun  9127  hsmex  9137  dominf  9150  zornn0g  9210  dominfac  9274  wununi  9407  wunex2  9439  wuncval2  9448  incexclem  14407  mrcfval  16091  mrisval  16113  acsdrsel  16990  isacs4lem  16991  isacs5lem  16992  acsdrscl  16993  isps  17025  isdir  17055  sylow2a  17857  uniopn  20527  istopon  20540  eltg3  20577  tgdom  20593  indistopon  20615  cldval  20637  ntrfval  20638  clsfval  20639  mretopd  20706  neifval  20713  lpfval  20752  isperf  20765  tgrest  20773  ist0  20934  ist1  20935  ishaus  20936  iscnrm  20937  iscmp  21001  cmpcov  21002  cmpcovf  21004  cncmp  21005  fincmp  21006  cmpsublem  21012  cmpsub  21013  tgcmp  21014  cmpcld  21015  uncmp  21016  hauscmplem  21019  cmpfi  21021  iscon  21026  is1stc  21054  2ndc1stc  21064  2ndcsep  21072  isref  21122  isptfin  21129  islocfin  21130  comppfsc  21145  kgenval  21148  1stckgenlem  21166  txcmplem1  21254  txcmplem2  21255  kqval  21339  flffval  21603  fclsval  21622  fcfval  21647  alexsublem  21658  alexsubb  21660  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  ptcmplem2  21667  ptcmplem3  21668  ptcmplem5  21670  cnextval  21675  iscfilu  21902  icccmplem1  22433  icccmplem2  22434  bndth  22565  lebnumlem3  22570  om1val  22638  pi1val  22645  ovolicc2  23097  isplig  26720  hsupval  27577  acunirnmpt  28841  iscref  29239  crefi  29242  cmpcref  29245  pcmplfin  29255  sigaclcu  29507  prsiga  29521  sigaclci  29522  unelsiga  29524  sigagenval  29530  unelldsys  29548  sigapildsys  29552  ldgenpisyslem1  29553  rossros  29570  measvun  29599  ismbfm  29641  isanmbfm  29645  dya2iocuni  29672  oms0  29686  omssubadd  29689  carsgsigalem  29704  fiunelcarsg  29705  carsgclctunlem1  29706  carsgclctunlem2  29708  carsgclctunlem3  29709  carsgclctun  29710  pmeasmono  29713  pmeasadd  29714  kur14  30452  ispcon  30459  cvmscbv  30494  cvmsi  30501  cvmsval  30502  dfrdg2  30945  brbigcup  31175  dfbigcup2  31176  fobigcup  31177  brapply  31215  dfrdg4  31228  isfne  31504  fneval  31517  fnemeet1  31531  fnemeet2  31532  fnejoin1  31533  fnejoin2  31534  tailfval  31537  ordtoplem  31604  onsucsuccmpi  31612  limsucncmpi  31614  ordcmp  31616  dissneqlem  32363  finxpreclem3  32406  heicant  32614  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  mbfresfi  32626  cover2  32678  cover2g  32679  istotbnd3  32740  sstotbnd  32744  heiborlem1  32780  heiborlem6  32785  heiborlem8  32787  isnacs3  36291  nacsfix  36293  pwelg  36884  csbfv12gALTVD  38157  stoweidlem35  38928  stoweidlem39  38932  stoweidlem50  38943  stoweidlem57  38950  issal  39210  salunicl  39212  saluncl  39213  prsal  39214  salgenval  39217  intsaluni  39223  salgenn0  39225  salgencl  39226  sssalgen  39229  salgenss  39230  salgenuni  39231  issalgend  39232  dfsalgen2  39235  issalnnd  39239  meadjuni  39350  ismeannd  39360  omeunile  39395  caragenunicl  39414  isomennd  39421  issmflem  39613  onsetreclem1  42247