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

Theorem unieq 4476
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 3169 . . 3 (𝐴 = 𝐵 → (∃𝑥𝐴 𝑦𝑥 ↔ ∃𝑥𝐵 𝑦𝑥))
21abbidv 2770 . 2 (𝐴 = 𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥} = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥})
3 dfuni2 4470 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
4 dfuni2 4470 . 2 𝐵 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥}
52, 3, 43eqtr4g 2710 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  {cab 2637  wrex 2942   cuni 4468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-uni 4469
This theorem is referenced by:  unieqi  4477  unieqd  4478  uniintsn  4546  iununi  4642  treq  4791  elvvuni  5213  unielrel  5698  unixp0  5707  unixpid  5708  limeq  5773  unizlim  5882  opabiotafun  6298  uniex  6995  uniexg  6997  onsucuni2  7076  onuninsuci  7082  orduninsuc  7085  undefval  7447  en1b  8065  nnunifi  8252  fissuni  8312  infeq5i  8571  infeq5  8572  trcl  8642  rankuni  8764  rankxplim3  8782  iunfictbso  8975  cflim2  9123  cfss  9125  cfslb  9126  fin2i  9155  fin1a2lem10  9269  fin1a2lem11  9270  fin1a2lem12  9271  itunisuc  9279  ituniiun  9282  hsmex  9292  dominf  9305  zornn0g  9365  dominfac  9433  wununi  9566  wunex2  9598  wuncval2  9607  incexclem  14612  mrcfval  16315  mrisval  16337  acsdrsel  17214  isacs4lem  17215  isacs5lem  17216  acsdrscl  17217  isps  17249  isdir  17279  sylow2a  18080  uniopn  20750  istopon  20765  eltg3  20814  tgdom  20830  indistopon  20853  cldval  20875  ntrfval  20876  clsfval  20877  mretopd  20944  neifval  20951  lpfval  20990  isperf  21003  tgrest  21011  ist0  21172  ist1  21173  ishaus  21174  iscnrm  21175  iscmp  21239  cmpcov  21240  cmpcovf  21242  cncmp  21243  fincmp  21244  cmpsublem  21250  cmpsub  21251  tgcmp  21252  cmpcld  21253  uncmp  21254  hauscmplem  21257  cmpfi  21259  isconn  21264  is1stc  21292  2ndc1stc  21302  2ndcsep  21310  isref  21360  isptfin  21367  islocfin  21368  comppfsc  21383  kgenval  21386  1stckgenlem  21404  txcmplem1  21492  txcmplem2  21493  kqval  21577  flffval  21840  fclsval  21859  fcfval  21884  alexsublem  21895  alexsubb  21897  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  alexsubALT  21902  ptcmplem2  21904  ptcmplem3  21905  ptcmplem5  21907  cnextval  21912  iscfilu  22139  icccmplem1  22672  icccmplem2  22673  bndth  22804  lebnumlem3  22809  om1val  22876  pi1val  22883  ovolicc2  23336  isplig  27458  hsupval  28321  acunirnmpt  29587  iscref  30039  crefi  30042  cmpcref  30045  pcmplfin  30055  sigaclcu  30308  prsiga  30322  sigaclci  30323  unelsiga  30325  sigagenval  30331  unelldsys  30349  sigapildsys  30353  ldgenpisyslem1  30354  rossros  30371  measvun  30400  ismbfm  30442  isanmbfm  30446  dya2iocuni  30473  oms0  30487  omssubadd  30490  carsgsigalem  30505  fiunelcarsg  30506  carsgclctunlem1  30507  carsgclctunlem2  30509  carsgclctunlem3  30510  carsgclctun  30511  pmeasmono  30514  pmeasadd  30515  kur14  31324  ispconn  31331  cvmscbv  31366  cvmsi  31373  cvmsval  31374  dfrdg2  31825  brbigcup  32130  dfbigcup2  32131  fobigcup  32132  brapply  32170  dfrdg4  32183  isfne  32459  fneval  32472  fnemeet1  32486  fnemeet2  32487  fnejoin1  32488  fnejoin2  32489  tailfval  32492  ordtoplem  32559  onsucsuccmpi  32567  limsucncmpi  32569  ordcmp  32571  bj-ismoore  33184  dissneqlem  33317  finxpreclem3  33360  heicant  33574  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  mbfresfi  33586  cover2  33638  cover2g  33639  istotbnd3  33700  sstotbnd  33704  heiborlem1  33740  heiborlem6  33745  heiborlem8  33747  isnacs3  37590  nacsfix  37592  pwelg  38182  csbfv12gALTVD  39449  stoweidlem35  40570  stoweidlem39  40574  stoweidlem50  40585  stoweidlem57  40592  issal  40852  salunicl  40854  saluncl  40855  prsal  40856  salgenval  40859  intsaluni  40865  salgenn0  40867  salgencl  40868  sssalgen  40871  salgenss  40872  salgenuni  40873  issalgend  40874  dfsalgen2  40877  issalnnd  40881  meadjuni  40992  ismeannd  41002  omeunile  41040  caragenunicl  41059  isomennd  41066  issmflem  41257  onsetreclem1  42776
  Copyright terms: Public domain W3C validator