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

Theorem unieq 4370
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 3111 . . 3 (𝐴 = 𝐵 → (∃𝑥𝐴 𝑦𝑥 ↔ ∃𝑥𝐵 𝑦𝑥))
21abbidv 2723 . 2 (𝐴 = 𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥} = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥})
3 dfuni2 4364 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
4 dfuni2 4364 . 2 𝐵 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥}
52, 3, 43eqtr4g 2664 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  {cab 2591  wrex 2892   cuni 4362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rex 2897  df-uni 4363
This theorem is referenced by:  unieqi  4371  unieqd  4372  uniintsn  4439  iununi  4536  treq  4676  elvvuni  5088  unielrel  5559  unixp0  5568  unixpid  5569  limeq  5634  unizlim  5743  opabiotafun  6150  uniex  6824  uniexg  6826  onsucuni2  6899  onuninsuci  6905  orduninsuc  6908  undefval  7262  en1b  7883  nnunifi  8069  fissuni  8127  infeq5i  8389  infeq5  8390  trcl  8460  rankuni  8582  rankxplim3  8600  iunfictbso  8793  cflim2  8941  cfss  8943  cfslb  8944  fin2i  8973  fin1a2lem10  9087  fin1a2lem11  9088  fin1a2lem12  9089  itunisuc  9097  ituniiun  9100  hsmex  9110  dominf  9123  zornn0g  9183  dominfac  9247  wununi  9380  wunex2  9412  wuncval2  9421  incexclem  14349  mrcfval  16033  mrisval  16055  acsdrsel  16932  isacs4lem  16933  isacs5lem  16934  acsdrscl  16935  isps  16967  isdir  16997  sylow2a  17799  uniopn  20465  istopon  20478  eltg3  20515  tgdom  20531  indistopon  20553  cldval  20575  ntrfval  20576  clsfval  20577  mretopd  20644  neifval  20651  lpfval  20690  isperf  20703  tgrest  20711  ist0  20872  ist1  20873  ishaus  20874  iscnrm  20875  iscmp  20939  cmpcov  20940  cmpcovf  20942  cncmp  20943  fincmp  20944  cmpsublem  20950  cmpsub  20951  tgcmp  20952  cmpcld  20953  uncmp  20954  hauscmplem  20957  cmpfi  20959  iscon  20964  is1stc  20992  2ndc1stc  21002  2ndcsep  21010  isref  21060  isptfin  21067  islocfin  21068  comppfsc  21083  kgenval  21086  1stckgenlem  21104  txcmplem1  21192  txcmplem2  21193  kqval  21277  flffval  21541  fclsval  21560  fcfval  21585  alexsublem  21596  alexsubb  21598  alexsubALTlem2  21600  alexsubALTlem3  21601  alexsubALTlem4  21602  alexsubALT  21603  ptcmplem2  21605  ptcmplem3  21606  ptcmplem5  21608  cnextval  21613  iscfilu  21840  icccmplem1  22361  icccmplem2  22362  bndth  22492  lebnumlem3  22497  om1val  22565  pi1val  22572  ovolicc2  23010  isplig  26482  hsupval  27379  acunirnmpt  28643  iscref  29041  crefi  29044  cmpcref  29047  pcmplfin  29057  sigaclcu  29309  prsiga  29323  sigaclci  29324  unelsiga  29326  sigagenval  29332  unelldsys  29350  sigapildsys  29354  ldgenpisyslem1  29355  rossros  29372  measvun  29401  ismbfm  29443  isanmbfm  29447  dya2iocuni  29474  oms0  29488  omssubadd  29491  carsgsigalem  29506  fiunelcarsg  29507  carsgclctunlem1  29508  carsgclctunlem2  29510  carsgclctunlem3  29511  carsgclctun  29512  pmeasmono  29515  pmeasadd  29516  kur14  30254  ispcon  30261  cvmscbv  30296  cvmsi  30303  cvmsval  30304  dfrdg2  30747  brbigcup  30977  dfbigcup2  30978  fobigcup  30979  brapply  31017  dfrdg4  31030  isfne  31306  fneval  31319  fnemeet1  31333  fnemeet2  31334  fnejoin1  31335  fnejoin2  31336  tailfval  31339  ordtoplem  31406  onsucsuccmpi  31414  limsucncmpi  31416  ordcmp  31418  dissneqlem  32162  finxpreclem3  32205  heicant  32413  ovoliunnfl  32420  voliunnfl  32422  volsupnfl  32423  mbfresfi  32425  cover2  32477  cover2g  32478  istotbnd3  32539  sstotbnd  32543  heiborlem1  32579  heiborlem6  32584  heiborlem8  32586  isnacs3  36090  nacsfix  36092  pwelg  36683  csbfv12gALTVD  37956  stoweidlem35  38728  stoweidlem39  38732  stoweidlem50  38743  stoweidlem57  38750  issal  39010  salunicl  39012  saluncl  39013  prsal  39014  salgenval  39017  intsaluni  39023  salgenn0  39025  salgencl  39026  sssalgen  39029  salgenss  39030  salgenuni  39031  issalgend  39032  dfsalgen2  39035  issalnnd  39039  meadjuni  39150  ismeannd  39160  omeunile  39195  caragenunicl  39214  isomennd  39221  issmflem  39413
  Copyright terms: Public domain W3C validator