Theorem unieq 4666

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 3351	. . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝑥))
2	1	abbidv 2946	. 2 ⊢ (𝐴 = 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝑥})
3		dfuni2 4660	. 2 ⊢ ∪ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
4		dfuni2 4660	. 2 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝑥}
5	2, 3, 4	3eqtr4g 2886	1 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1658  {cab 2811  ∃wrex 3118  ∪ cuni 4658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-uni 4659

This theorem is referenced by:  unieqi  4667  unieqd  4668  uniintsn  4734  iununi  4831  treq  4981  elvvuni  5412  unielrel  5901  unixp0  5910  unixpid  5911  limeq  5975  unizlim  6079  opabiotafun  6506  uniex  7213  uniexg  7215  onsucuni2  7295  onuninsuci  7301  orduninsuc  7304  undefval  7667  en1b  8290  nnunifi  8480  fissuni  8540  infeq5i  8810  infeq5  8811  trcl  8881  rankuni  9003  rankxplim3  9021  iunfictbso  9250  cflim2  9400  cfss  9402  cfslb  9403  fin2i  9432  fin1a2lem10  9546  fin1a2lem11  9547  fin1a2lem12  9548  itunisuc  9556  ituniiun  9559  hsmex  9569  dominf  9582  zornn0g  9642  dominfac  9710  wununi  9843  wunex2  9875  wuncval2  9884  incexclem  14942  mrcfval  16621  mrisval  16643  acsdrsel  17520  isacs4lem  17521  isacs5lem  17522  acsdrscl  17523  isps  17555  isdir  17585  sylow2a  18385  uniopn  21072  istopon  21087  eltg3  21137  tgdom  21153  indistopon  21176  cldval  21198  ntrfval  21199  clsfval  21200  mretopd  21267  neifval  21274  lpfval  21313  isperf  21326  tgrest  21334  ist0  21495  ist1  21496  ishaus  21497  iscnrm  21498  iscmp  21562  cmpcov  21563  cmpcovf  21565  cncmp  21566  fincmp  21567  cmpsublem  21573  cmpsub  21574  tgcmp  21575  cmpcld  21576  uncmp  21577  hauscmplem  21580  cmpfi  21582  isconn  21587  is1stc  21615  2ndc1stc  21625  2ndcsep  21633  isref  21683  isptfin  21690  islocfin  21691  comppfsc  21706  kgenval  21709  1stckgenlem  21727  txcmplem1  21815  txcmplem2  21816  kqval  21900  flffval  22163  fclsval  22182  fcfval  22207  alexsublem  22218  alexsubb  22220  alexsubALTlem2  22222  alexsubALTlem3  22223  alexsubALTlem4  22224  alexsubALT  22225  ptcmplem2  22227  ptcmplem3  22228  ptcmplem5  22230  cnextval  22235  iscfilu  22462  icccmplem1  22995  icccmplem2  22996  bndth  23127  lebnumlem3  23132  om1val  23199  pi1val  23206  ovolicc2  23688  isplig  27886  hsupval  28748  acunirnmpt  30008  iscref  30456  crefi  30459  cmpcref  30462  pcmplfin  30472  sigaclcu  30725  prsiga  30739  sigaclci  30740  unelsiga  30742  sigagenval  30748  unelldsys  30766  sigapildsys  30770  ldgenpisyslem1  30771  rossros  30788  measvun  30817  ismbfm  30859  isanmbfm  30863  dya2iocuni  30890  oms0  30904  omssubadd  30907  carsgsigalem  30922  fiunelcarsg  30923  carsgclctunlem1  30924  carsgclctunlem2  30926  carsgclctunlem3  30927  carsgclctun  30928  pmeasmono  30931  pmeasadd  30932  kur14  31744  ispconn  31751  cvmscbv  31786  cvmsi  31793  cvmsval  31794  dfrdg2  32239  brbigcup  32544  dfbigcup2  32545  fobigcup  32546  brapply  32584  dfrdg4  32597  isfne  32872  fneval  32885  fnemeet1  32899  fnemeet2  32900  fnejoin1  32901  fnejoin2  32902  tailfval  32905  ordtoplem  32967  onsucsuccmpi  32975  limsucncmpi  32977  ordcmp  32979  bj-ismoore  33582  dissneqlem  33733  finxpreclem3  33775  heicant  33988  ovoliunnfl  33995  voliunnfl  33997  volsupnfl  33998  mbfresfi  33999  cover2  34051  cover2g  34052  istotbnd3  34112  sstotbnd  34116  heiborlem1  34152  heiborlem6  34157  heiborlem8  34159  isnacs3  38117  nacsfix  38119  pwelg  38706  csbfv12gALTVD  39953  stoweidlem35  41046  stoweidlem39  41050  stoweidlem50  41061  stoweidlem57  41068  issal  41325  salunicl  41327  saluncl  41328  prsal  41329  salgenval  41332  intsaluni  41338  salgenn0  41340  salgencl  41341  sssalgen  41344  salgenss  41345  salgenuni  41346  issalgend  41347  dfsalgen2  41350  issalnnd  41354  meadjuni  41465  ismeannd  41475  omeunile  41513  caragenunicl  41532  isomennd  41539  issmflem  41730  onsetreclem1  43346