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

Theorem unieqi 4639
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 4638 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637   cuni 4630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-uni 4631
This theorem is referenced by:  elunirab  4642  unisng  4645  unisnOLD  4647  unidif0  5030  univ  5109  uniop  5170  dfiun3g  5579  op1sta  5830  op2nda  5834  dfdm2  5881  unixpid  5884  unisuc  6014  iotajust  6063  dfiota2  6065  cbviota  6069  sb8iota  6071  dffv4  6405  funfv2f  6488  funiunfv  6730  elunirnALT  6734  riotauni  6841  ordunisuc  7262  1st0  7404  2nd0  7405  unielxp  7436  brtpos0  7594  dfrecs3  7705  recsfval  7713  tz7.44-3  7740  uniqs  8042  xpassen  8293  dffi3  8576  dfsup2  8589  sup00  8609  r1limg  8881  jech9.3  8924  rankxplim2  8990  rankxplim3  8991  rankxpsuc  8992  dfac5lem2  9230  kmlem11  9267  cflim2  9370  fin23lem30  9449  fin23lem34  9453  itunisuc  9526  itunitc  9528  ituniiun  9529  ac6num  9586  rankcf  9884  dprd2da  18643  dmdprdsplit2lem  18646  lssuni  19144  basdif0  20971  tgdif0  21010  neiptopuni  21148  restcls  21199  restntr  21200  pnrmopn  21361  cncmp  21409  discmp  21415  hauscmplem  21423  unisngl  21544  xkouni  21616  uptx  21642  ufildr  21948  ptcmplem3  22071  utop2nei  22267  utopreg  22269  zcld  22829  icccmp  22841  cncfcnvcn  22937  cnmpt2pc  22940  cnheibor  22967  evth  22971  evth2  22972  iunmbl  23534  voliun  23535  dvcnvrelem2  23995  ftc1  24019  aannenlem2  24298  circtopn  30229  locfinref  30233  tpr2rico  30283  cbvesum  30429  unibrsiga  30574  sxbrsigalem3  30659  dya2iocucvr  30671  sxbrsigalem1  30672  sibf0  30721  sibff  30723  sitgclg  30729  probfinmeasbOLD  30815  coinflipuniv  30868  cvmliftlem10  31599  dfon2lem7  32014  dfrdg2  32021  frrlem6  32110  frrlem7  32111  frrlem10  32112  frrlem11  32113  noetalem4  32187  dfiota3  32351  dffv5  32352  dfrecs2  32378  dfrdg4  32379  ordcmp  32763  bj-nuliotaALT  33330  mptsnun  33503  finxp1o  33545  ftc1cnnc  33796  uniqsALTV  34416  refsum2cnlem1  39690  lptre2pt  40352  limclner  40363  limclr  40367  stoweidlem62  40758  fourierdlem42  40845  fourierdlem80  40882  fouriercnp  40922  qndenserrn  40998  salexct3  41039  salgencntex  41040  salgensscntex  41041  subsalsal  41056  0ome  41225  borelmbl  41332  mbfresmf  41430  cnfsmf  41431  incsmf  41433  smfmbfcex  41450  decsmf  41457  smfpimbor1lem2  41488  setrec2  43010
  Copyright terms: Public domain W3C validator