MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unieq Structured version   Visualization version   GIF version

Theorem unieq 4845
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.
StepHypRef Expression
1 rexeq 3412 . . 3 (𝐴 = 𝐵 → (∃𝑥𝐴 𝑦𝑥 ↔ ∃𝑥𝐵 𝑦𝑥))
21abbidv 2890 . 2 (𝐴 = 𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥} = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥})
3 dfuni2 4839 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
4 dfuni2 4839 . 2 𝐵 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥}
52, 3, 43eqtr4g 2886 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  {cab 2804  wrex 3144   cuni 4837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-rex 3149  df-uni 4838
This theorem is referenced by:  unieqi  4846  unieqd  4847  uniintsn  4911  iununi  5018  treq  5175  elvvuni  5627  unielrel  6123  unixp0  6132  unixpid  6133  limeq  6201  unizlim  6305  opabiotafun  6741  uniex  7455  uniexg  7457  onsucuni2  7537  onuninsuci  7543  orduninsuc  7546  undefval  7933  en1b  8566  nnunifi  8758  fissuni  8818  infeq5i  9088  infeq5  9089  trcl  9159  rankuni  9281  rankxplim3  9299  iunfictbso  9529  cflim2  9674  cfss  9676  cfslb  9677  fin2i  9706  fin1a2lem10  9820  fin1a2lem11  9821  fin1a2lem12  9822  itunisuc  9830  ituniiun  9833  hsmex  9843  dominf  9856  zornn0g  9916  dominfac  9984  wununi  10117  wunex2  10149  wuncval2  10158  incexclem  15181  mrcfval  16869  mrisval  16891  acsdrsel  17767  isacs4lem  17768  isacs5lem  17769  acsdrscl  17770  isps  17802  isdir  17832  sylow2a  18664  uniopn  21421  istopon  21436  eltg3  21486  tgdom  21502  indistopon  21525  cldval  21547  ntrfval  21548  clsfval  21549  mretopd  21616  neifval  21623  lpfval  21662  isperf  21675  tgrest  21683  ist0  21844  ist1  21845  ishaus  21846  iscnrm  21847  iscmp  21912  cmpcov  21913  cmpcovf  21915  cncmp  21916  fincmp  21917  cmpsublem  21923  cmpsub  21924  tgcmp  21925  cmpcld  21926  uncmp  21927  hauscmplem  21930  cmpfi  21932  isconn  21937  is1stc  21965  2ndc1stc  21975  2ndcsep  21983  isref  22033  isptfin  22040  islocfin  22041  comppfsc  22056  kgenval  22059  1stckgenlem  22077  txcmplem1  22165  txcmplem2  22166  kqval  22250  flffval  22513  fclsval  22532  fcfval  22557  alexsublem  22568  alexsubb  22570  alexsubALTlem2  22572  alexsubALTlem3  22573  alexsubALTlem4  22574  alexsubALT  22575  ptcmplem2  22577  ptcmplem3  22578  ptcmplem5  22580  cnextval  22585  iscfilu  22812  icccmplem1  23345  icccmplem2  23346  bndth  23477  lebnumlem3  23482  om1val  23549  pi1val  23556  ovolicc2  24038  isplig  28167  hsupval  29025  acunirnmpt  30319  iscref  30994  crefi  30997  cmpcref  31000  pcmplfin  31010  sigaclcu  31262  prsiga  31276  sigaclci  31277  unelsiga  31279  sigagenval  31285  unelldsys  31303  sigapildsys  31307  ldgenpisyslem1  31308  rossros  31325  measvun  31354  ismbfm  31396  isanmbfm  31400  dya2iocuni  31427  oms0  31441  omssubadd  31444  carsgsigalem  31459  fiunelcarsg  31460  carsgclctunlem1  31461  carsgclctunlem2  31463  carsgclctunlem3  31464  carsgclctun  31465  pmeasmono  31468  pmeasadd  31469  kur14  32347  ispconn  32354  cvmscbv  32389  cvmsi  32396  cvmsval  32397  dfrdg2  32924  brbigcup  33243  dfbigcup2  33244  fobigcup  33245  brapply  33283  dfrdg4  33296  isfne  33571  fneval  33584  fnemeet1  33598  fnemeet2  33599  fnejoin1  33600  fnejoin2  33601  tailfval  33604  ordtoplem  33667  onsucsuccmpi  33675  limsucncmpi  33677  ordcmp  33679  bj-ismoore  34278  dissneqlem  34490  finxpreclem3  34543  pibp19  34564  pibp21  34565  pibt2  34567  heicant  34794  ovoliunnfl  34801  voliunnfl  34803  volsupnfl  34804  mbfresfi  34805  cover2  34857  cover2g  34858  istotbnd3  34917  sstotbnd  34921  heiborlem1  34957  heiborlem6  34962  heiborlem8  34964  dmqseqim  35757  isnacs3  39172  nacsfix  39174  pwelg  39784  mnuprdlem1  40473  mnuprdlem2  40474  mnuunid  40478  mnurndlem1  40482  csbfv12gALTVD  41098  stoweidlem35  42186  stoweidlem39  42190  stoweidlem50  42201  stoweidlem57  42208  issal  42465  salunicl  42467  saluncl  42468  prsal  42469  salgenval  42472  intsaluni  42478  salgenn0  42480  salgencl  42481  sssalgen  42484  salgenss  42485  salgenuni  42486  issalgend  42487  dfsalgen2  42490  issalnnd  42494  meadjuni  42605  ismeannd  42615  omeunile  42653  caragenunicl  42672  isomennd  42679  issmflem  42870  onsetreclem1  44639
  Copyright terms: Public domain W3C validator