Theorem unieq 4444

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

Syntax hints:   → wi 4   = wceq 1483  {cab 2608  ∃wrex 2913  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437

This theorem is referenced by:  unieqi  4445  unieqd  4446  uniintsn  4514  iununi  4610  treq  4758  elvvuni  5179  unielrel  5660  unixp0  5669  unixpid  5670  limeq  5735  unizlim  5844  opabiotafun  6259  uniex  6953  uniexg  6955  onsucuni2  7034  onuninsuci  7040  orduninsuc  7043  undefval  7402  en1b  8024  nnunifi  8211  fissuni  8271  infeq5i  8533  infeq5  8534  trcl  8604  rankuni  8726  rankxplim3  8744  iunfictbso  8937  cflim2  9085  cfss  9087  cfslb  9088  fin2i  9117  fin1a2lem10  9231  fin1a2lem11  9232  fin1a2lem12  9233  itunisuc  9241  ituniiun  9244  hsmex  9254  dominf  9267  zornn0g  9327  dominfac  9395  wununi  9528  wunex2  9560  wuncval2  9569  incexclem  14568  mrcfval  16268  mrisval  16290  acsdrsel  17167  isacs4lem  17168  isacs5lem  17169  acsdrscl  17170  isps  17202  isdir  17232  sylow2a  18034  uniopn  20702  istopon  20717  eltg3  20766  tgdom  20782  indistopon  20805  cldval  20827  ntrfval  20828  clsfval  20829  mretopd  20896  neifval  20903  lpfval  20942  isperf  20955  tgrest  20963  ist0  21124  ist1  21125  ishaus  21126  iscnrm  21127  iscmp  21191  cmpcov  21192  cmpcovf  21194  cncmp  21195  fincmp  21196  cmpsublem  21202  cmpsub  21203  tgcmp  21204  cmpcld  21205  uncmp  21206  hauscmplem  21209  cmpfi  21211  isconn  21216  is1stc  21244  2ndc1stc  21254  2ndcsep  21262  isref  21312  isptfin  21319  islocfin  21320  comppfsc  21335  kgenval  21338  1stckgenlem  21356  txcmplem1  21444  txcmplem2  21445  kqval  21529  flffval  21793  fclsval  21812  fcfval  21837  alexsublem  21848  alexsubb  21850  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  ptcmplem2  21857  ptcmplem3  21858  ptcmplem5  21860  cnextval  21865  iscfilu  22092  icccmplem1  22625  icccmplem2  22626  bndth  22757  lebnumlem3  22762  om1val  22830  pi1val  22837  ovolicc2  23290  isplig  27328  hsupval  28193  acunirnmpt  29459  iscref  29911  crefi  29914  cmpcref  29917  pcmplfin  29927  sigaclcu  30180  prsiga  30194  sigaclci  30195  unelsiga  30197  sigagenval  30203  unelldsys  30221  sigapildsys  30225  ldgenpisyslem1  30226  rossros  30243  measvun  30272  ismbfm  30314  isanmbfm  30318  dya2iocuni  30345  oms0  30359  omssubadd  30362  carsgsigalem  30377  fiunelcarsg  30378  carsgclctunlem1  30379  carsgclctunlem2  30381  carsgclctunlem3  30382  carsgclctun  30383  pmeasmono  30386  pmeasadd  30387  kur14  31198  ispconn  31205  cvmscbv  31240  cvmsi  31247  cvmsval  31248  dfrdg2  31701  brbigcup  32005  dfbigcup2  32006  fobigcup  32007  brapply  32045  dfrdg4  32058  isfne  32334  fneval  32347  fnemeet1  32361  fnemeet2  32362  fnejoin1  32363  fnejoin2  32364  tailfval  32367  ordtoplem  32434  onsucsuccmpi  32442  limsucncmpi  32444  ordcmp  32446  bj-ismoore  33059  dissneqlem  33187  finxpreclem3  33230  heicant  33444  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  mbfresfi  33456  cover2  33508  cover2g  33509  istotbnd3  33570  sstotbnd  33574  heiborlem1  33610  heiborlem6  33615  heiborlem8  33617  isnacs3  37273  nacsfix  37275  pwelg  37865  csbfv12gALTVD  39135  stoweidlem35  40252  stoweidlem39  40256  stoweidlem50  40267  stoweidlem57  40274  issal  40534  salunicl  40536  saluncl  40537  prsal  40538  salgenval  40541  intsaluni  40547  salgenn0  40549  salgencl  40550  sssalgen  40553  salgenss  40554  salgenuni  40555  issalgend  40556  dfsalgen2  40559  issalnnd  40563  meadjuni  40674  ismeannd  40684  omeunile  40719  caragenunicl  40738  isomennd  40745  issmflem  40936  onsetreclem1  42448