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

Theorem unieqi 4258
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 4257 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  U.cuni 4249
This theorem is referenced by:  elunirab  4261  unisn  4264  unidif0  4625  univ  4703  uniop  4755  unisuc  4959  dfiun3g  5260  op1sta  5495  op2nda  5498  dfdm2  5544  unixpid  5547  iotajust  5555  dfiota2  5557  cbviota  5561  sb8iota  5563  dffv4  5868  funfv2f  5942  funiunfv  6160  elunirnALT  6164  riotauni  6263  ordunisuc  6667  1st0  6806  2nd0  6807  unielxp  6836  brtpos0  6981  recsfval  7069  tz7.44-3  7093  uniqs  7390  xpassen  7631  dffi3  7911  dfsup2  7922  dfsup2OLD  7923  dfsup3OLD  7924  r1limg  8210  jech9.3  8253  rankxplim2  8319  rankxplim3  8320  rankxpsuc  8321  dfac5lem2  8526  kmlem11  8561  cflim2  8664  fin23lem30  8743  fin23lem34  8747  itunisuc  8820  itunitc  8822  ituniiun  8823  ac6num  8880  rankcf  9176  dprd2da  17091  dmdprdsplit2lem  17094  lssuni  17586  basdif0  19454  tgdif0  19494  neiptopuni  19631  restcls  19682  restntr  19683  pnrmopn  19844  cncmp  19892  discmp  19898  hauscmplem  19906  unisngl  20028  xkouni  20100  uptx  20126  ufildr  20432  ptcmplem3  20554  utop2nei  20753  utopreg  20755  zcld  21318  icccmp  21330  cncfcnvcn  21425  cnmpt2pc  21428  cnheibor  21455  evth  21459  evth2  21460  iunmbl  21963  voliun  21964  dvcnvrelem2  22419  ftc1  22443  aannenlem2  22725  circtopn  27840  locfinref  27844  tpr2rico  27894  cbvesum  28054  unibrsiga  28157  sxbrsigalem3  28243  dya2iocucvr  28255  sxbrsigalem1  28256  sibf0  28276  sibff  28278  sitgclg  28284  probfinmeasbOLD  28367  coinflipuniv  28420  cvmliftlem10  28739  dfon2lem7  29221  dfrdg2  29228  frrlem11  29399  dfiota3  29573  dffv5  29574  dfrdg4  29600  ordcmp  29912  ftc1cnnc  30089  refsum2cnlem1  31412  lptre2pt  31646  limclner  31657  limclr  31661  stoweidlem62  31844  fourierdlem42  31931  fourierdlem80  31969  fouriercnp  32009  bj-nuliotaALT  34587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-uni 4250
  Copyright terms: Public domain W3C validator