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

Theorem unieq 4442
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 3137 . . 3 (𝐴 = 𝐵 → (∃𝑥𝐴 𝑦𝑥 ↔ ∃𝑥𝐵 𝑦𝑥))
21abbidv 2740 . 2 (𝐴 = 𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥} = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥})
3 dfuni2 4436 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
4 dfuni2 4436 . 2 𝐵 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥}
52, 3, 43eqtr4g 2680 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  {cab 2607  wrex 2912   cuni 4434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rex 2917  df-uni 4435
This theorem is referenced by:  unieqi  4443  unieqd  4444  uniintsn  4512  iununi  4608  treq  4756  elvvuni  5177  unielrel  5658  unixp0  5667  unixpid  5668  limeq  5733  unizlim  5842  opabiotafun  6257  uniex  6950  uniexg  6952  onsucuni2  7031  onuninsuci  7037  orduninsuc  7040  undefval  7399  en1b  8021  nnunifi  8208  fissuni  8268  infeq5i  8530  infeq5  8531  trcl  8601  rankuni  8723  rankxplim3  8741  iunfictbso  8934  cflim2  9082  cfss  9084  cfslb  9085  fin2i  9114  fin1a2lem10  9228  fin1a2lem11  9229  fin1a2lem12  9230  itunisuc  9238  ituniiun  9241  hsmex  9251  dominf  9264  zornn0g  9324  dominfac  9392  wununi  9525  wunex2  9557  wuncval2  9566  incexclem  14562  mrcfval  16262  mrisval  16284  acsdrsel  17161  isacs4lem  17162  isacs5lem  17163  acsdrscl  17164  isps  17196  isdir  17226  sylow2a  18028  uniopn  20696  istopon  20711  eltg3  20760  tgdom  20776  indistopon  20799  cldval  20821  ntrfval  20822  clsfval  20823  mretopd  20890  neifval  20897  lpfval  20936  isperf  20949  tgrest  20957  ist0  21118  ist1  21119  ishaus  21120  iscnrm  21121  iscmp  21185  cmpcov  21186  cmpcovf  21188  cncmp  21189  fincmp  21190  cmpsublem  21196  cmpsub  21197  tgcmp  21198  cmpcld  21199  uncmp  21200  hauscmplem  21203  cmpfi  21205  isconn  21210  is1stc  21238  2ndc1stc  21248  2ndcsep  21256  isref  21306  isptfin  21313  islocfin  21314  comppfsc  21329  kgenval  21332  1stckgenlem  21350  txcmplem1  21438  txcmplem2  21439  kqval  21523  flffval  21787  fclsval  21806  fcfval  21831  alexsublem  21842  alexsubb  21844  alexsubALTlem2  21846  alexsubALTlem3  21847  alexsubALTlem4  21848  alexsubALT  21849  ptcmplem2  21851  ptcmplem3  21852  ptcmplem5  21854  cnextval  21859  iscfilu  22086  icccmplem1  22619  icccmplem2  22620  bndth  22751  lebnumlem3  22756  om1val  22824  pi1val  22831  ovolicc2  23284  isplig  27312  hsupval  28177  acunirnmpt  29443  iscref  29896  crefi  29899  cmpcref  29902  pcmplfin  29912  sigaclcu  30165  prsiga  30179  sigaclci  30180  unelsiga  30182  sigagenval  30188  unelldsys  30206  sigapildsys  30210  ldgenpisyslem1  30211  rossros  30228  measvun  30257  ismbfm  30299  isanmbfm  30303  dya2iocuni  30330  oms0  30344  omssubadd  30347  carsgsigalem  30362  fiunelcarsg  30363  carsgclctunlem1  30364  carsgclctunlem2  30366  carsgclctunlem3  30367  carsgclctun  30368  pmeasmono  30371  pmeasadd  30372  kur14  31183  ispconn  31190  cvmscbv  31225  cvmsi  31232  cvmsval  31233  dfrdg2  31685  brbigcup  31989  dfbigcup2  31990  fobigcup  31991  brapply  32029  dfrdg4  32042  isfne  32318  fneval  32331  fnemeet1  32345  fnemeet2  32346  fnejoin1  32347  fnejoin2  32348  tailfval  32351  ordtoplem  32418  onsucsuccmpi  32426  limsucncmpi  32428  ordcmp  32430  bj-ismoore  33043  dissneqlem  33167  finxpreclem3  33210  heicant  33424  ovoliunnfl  33431  voliunnfl  33433  volsupnfl  33434  mbfresfi  33436  cover2  33488  cover2g  33489  istotbnd3  33550  sstotbnd  33554  heiborlem1  33590  heiborlem6  33595  heiborlem8  33597  isnacs3  37099  nacsfix  37101  pwelg  37691  csbfv12gALTVD  38961  stoweidlem35  40021  stoweidlem39  40025  stoweidlem50  40036  stoweidlem57  40043  issal  40303  salunicl  40305  saluncl  40306  prsal  40307  salgenval  40310  intsaluni  40316  salgenn0  40318  salgencl  40319  sssalgen  40322  salgenss  40323  salgenuni  40324  issalgend  40325  dfsalgen2  40328  issalnnd  40332  meadjuni  40443  ismeannd  40453  omeunile  40488  caragenunicl  40507  isomennd  40514  issmflem  40705  onsetreclem1  42219
  Copyright terms: Public domain W3C validator