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

Theorem unieq 4602
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 3287 . . 3 (𝐴 = 𝐵 → (∃𝑥𝐴 𝑦𝑥 ↔ ∃𝑥𝐵 𝑦𝑥))
21abbidv 2884 . 2 (𝐴 = 𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥} = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥})
3 dfuni2 4596 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
4 dfuni2 4596 . 2 𝐵 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥}
52, 3, 43eqtr4g 2824 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  {cab 2751  wrex 3056   cuni 4594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rex 3061  df-uni 4595
This theorem is referenced by:  unieqi  4603  unieqd  4604  uniintsn  4670  iununi  4767  treq  4917  elvvuni  5347  unielrel  5846  unixp0  5855  unixpid  5856  limeq  5920  unizlim  6024  opabiotafun  6448  uniex  7151  uniexg  7153  onsucuni2  7232  onuninsuci  7238  orduninsuc  7241  undefval  7605  en1b  8228  nnunifi  8418  fissuni  8478  infeq5i  8748  infeq5  8749  trcl  8819  rankuni  8941  rankxplim3  8959  iunfictbso  9188  cflim2  9338  cfss  9340  cfslb  9341  fin2i  9370  fin1a2lem10  9484  fin1a2lem11  9485  fin1a2lem12  9486  itunisuc  9494  ituniiun  9497  hsmex  9507  dominf  9520  zornn0g  9580  dominfac  9648  wununi  9781  wunex2  9813  wuncval2  9822  incexclem  14854  mrcfval  16536  mrisval  16558  acsdrsel  17435  isacs4lem  17436  isacs5lem  17437  acsdrscl  17438  isps  17470  isdir  17500  sylow2a  18300  uniopn  20981  istopon  20996  eltg3  21046  tgdom  21062  indistopon  21085  cldval  21107  ntrfval  21108  clsfval  21109  mretopd  21176  neifval  21183  lpfval  21222  isperf  21235  tgrest  21243  ist0  21404  ist1  21405  ishaus  21406  iscnrm  21407  iscmp  21471  cmpcov  21472  cmpcovf  21474  cncmp  21475  fincmp  21476  cmpsublem  21482  cmpsub  21483  tgcmp  21484  cmpcld  21485  uncmp  21486  hauscmplem  21489  cmpfi  21491  isconn  21496  is1stc  21524  2ndc1stc  21534  2ndcsep  21542  isref  21592  isptfin  21599  islocfin  21600  comppfsc  21615  kgenval  21618  1stckgenlem  21636  txcmplem1  21724  txcmplem2  21725  kqval  21809  flffval  22072  fclsval  22091  fcfval  22116  alexsublem  22127  alexsubb  22129  alexsubALTlem2  22131  alexsubALTlem3  22132  alexsubALTlem4  22133  alexsubALT  22134  ptcmplem2  22136  ptcmplem3  22137  ptcmplem5  22139  cnextval  22144  iscfilu  22371  icccmplem1  22904  icccmplem2  22905  bndth  23036  lebnumlem3  23041  om1val  23108  pi1val  23115  ovolicc2  23580  isplig  27722  hsupval  28584  acunirnmpt  29844  iscref  30293  crefi  30296  cmpcref  30299  pcmplfin  30309  sigaclcu  30562  prsiga  30576  sigaclci  30577  unelsiga  30579  sigagenval  30585  unelldsys  30603  sigapildsys  30607  ldgenpisyslem1  30608  rossros  30625  measvun  30654  ismbfm  30696  isanmbfm  30700  dya2iocuni  30727  oms0  30741  omssubadd  30744  carsgsigalem  30759  fiunelcarsg  30760  carsgclctunlem1  30761  carsgclctunlem2  30763  carsgclctunlem3  30764  carsgclctun  30765  pmeasmono  30768  pmeasadd  30769  kur14  31578  ispconn  31585  cvmscbv  31620  cvmsi  31627  cvmsval  31628  dfrdg2  32076  brbigcup  32381  dfbigcup2  32382  fobigcup  32383  brapply  32421  dfrdg4  32434  isfne  32709  fneval  32722  fnemeet1  32736  fnemeet2  32737  fnejoin1  32738  fnejoin2  32739  tailfval  32742  ordtoplem  32805  onsucsuccmpi  32813  limsucncmpi  32815  ordcmp  32817  bj-ismoore  33419  dissneqlem  33553  finxpreclem3  33595  heicant  33800  ovoliunnfl  33807  voliunnfl  33809  volsupnfl  33810  mbfresfi  33811  cover2  33863  cover2g  33864  istotbnd3  33924  sstotbnd  33928  heiborlem1  33964  heiborlem6  33969  heiborlem8  33971  isnacs3  37883  nacsfix  37885  pwelg  38472  csbfv12gALTVD  39719  stoweidlem35  40821  stoweidlem39  40825  stoweidlem50  40836  stoweidlem57  40843  issal  41103  salunicl  41105  saluncl  41106  prsal  41107  salgenval  41110  intsaluni  41116  salgenn0  41118  salgencl  41119  sssalgen  41122  salgenss  41123  salgenuni  41124  issalgend  41125  dfsalgen2  41128  issalnnd  41132  meadjuni  41243  ismeannd  41253  omeunile  41291  caragenunicl  41310  isomennd  41317  issmflem  41508  onsetreclem1  43052
  Copyright terms: Public domain W3C validator