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

Theorem unieqi 4846
Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
unieqi.1 𝐴 = 𝐵
Assertion
Ref Expression
unieqi 𝐴 = 𝐵

Proof of Theorem unieqi
StepHypRef Expression
1 unieqi.1 . 2 𝐴 = 𝐵
2 unieq 4845 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530   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:  elunirab  4849  unisng  4852  unidif0  5257  univ  5340  uniop  5402  dfiun3g  5834  op1sta  6080  op2nda  6083  dfdm2  6130  unixpid  6133  unisuc  6265  iotajust  6311  dfiota2  6313  cbviotaw  6319  cbviota  6321  sb8iota  6323  dffv4  6664  funfv2f  6749  funiunfv  7001  elunirnALT  7005  riotauni  7112  ordunisuc  7535  1st0  7686  2nd0  7687  unielxp  7718  brtpos0  7890  dfrecs3  8000  recsfval  8008  tz7.44-3  8035  uniqs  8347  xpassen  8600  dffi3  8884  dfsup2  8897  sup00  8917  r1limg  9189  jech9.3  9232  rankxplim2  9298  rankxplim3  9299  rankxpsuc  9300  dfac5lem2  9539  kmlem11  9575  cflim2  9674  fin23lem30  9753  fin23lem34  9757  itunisuc  9830  itunitc  9832  ituniiun  9833  ac6num  9890  rankcf  10188  dprd2da  19084  dmdprdsplit2lem  19087  lssuni  19631  basdif0  21477  tgdif0  21516  neiptopuni  21654  restcls  21705  restntr  21706  pnrmopn  21867  cncmp  21916  discmp  21922  hauscmplem  21930  unisngl  22051  xkouni  22123  uptx  22149  ufildr  22455  ptcmplem3  22578  utop2nei  22774  utopreg  22776  zcld  23336  icccmp  23348  cncfcnvcn  23444  cnmpopc  23447  cnheibor  23474  evth  23478  evth2  23479  iunmbl  24069  voliun  24070  dvcnvrelem2  24530  ftc1  24554  aannenlem2  24833  circtopn  30987  locfinref  30991  tpr2rico  31041  cbvesum  31187  unibrsiga  31331  sxbrsigalem3  31416  dya2iocucvr  31428  sxbrsigalem1  31429  sibf0  31478  sibff  31480  sitgclg  31486  probfinmeasbALTV  31573  coinflipuniv  31625  cvmliftlem10  32425  dfon2lem7  32918  dfrdg2  32924  frrlem5  33011  frrlem8  33014  frrlem10  33016  noetalem4  33104  dfiota3  33268  dffv5  33269  dfrecs2  33295  dfrdg4  33296  ordcmp  33679  bj-nuliotaALT  34232  mptsnun  34489  finxp1o  34542  ftc1cnnc  34833  uniqsALTV  35454  cnvepima  35462  dfom6  39763  refsum2cnlem1  41159  lptre2pt  41786  limclner  41797  limclr  41801  stoweidlem62  42213  fourierdlem42  42300  fourierdlem80  42337  fouriercnp  42377  qndenserrn  42450  salexct3  42491  salgencntex  42492  salgensscntex  42493  subsalsal  42508  0ome  42677  borelmbl  42784  mbfresmf  42882  cnfsmf  42883  incsmf  42885  smfmbfcex  42902  decsmf  42909  smfpimbor1lem2  42940  setrec2  44630
  Copyright terms: Public domain W3C validator