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

Theorem uneq2i 4139
Description: Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
uneq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
uneq2i (𝐶𝐴) = (𝐶𝐵)

Proof of Theorem uneq2i
StepHypRef Expression
1 uneq1i.1 . 2 𝐴 = 𝐵
2 uneq2 4136 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  cun 3937
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 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-v 3501  df-un 3944
This theorem is referenced by:  un4  4148  unundir  4150  difdif2  4264  difun2  4431  difdifdir  4439  dfif5  4485  qdass  4687  qdassr  4688  ssunpr  4763  iununi  5017  unidif0  5256  difxp1  6019  unisuc  6264  iunsuc  6270  fresaun  6545  fresaunres2  6546  fvssunirn  6695  fmptap  6927  fvsnun1  6941  fvsnun1OLD  6943  funiunfv  7004  onuninsuci  7546  wfrlem13  7961  wfrlem14  7962  wfrlem16  7964  tfrlem10  8017  oarec  8181  dfdom2  8527  fodomr  8660  ranksuc  9286  kmlem3  9570  djuassen  9596  fin1a2lem10  9823  fin1a2lem12  9825  axdc3lem4  9867  prunioo  12860  fz0sn0fz1  13017  facnn  13628  fac0  13629  hashun3  13738  trclublem  14348  dmtrclfv  14371  fsum2dlem  15117  fsumiun  15168  incexclem  15183  fprod2dlem  15326  prmreclem4  16247  phlstr  16645  mreexexlem4d  16910  opsrtoslem2  20185  restcld  21696  neitr  21704  fiuncmp  21928  refun0  22039  1stckgenlem  22077  filconn  22407  ufildr  22455  alexsubALTlem3  22573  ptcmplem1  22576  restmetu  23095  ovolfiniun  24017  unmbl  24053  volfiniun  24063  voliunlem1  24066  plyun0  24702  lgsquadlem3  25872  axlowdimlem3  26645  axlowdimlem17  26659  ex-un  28118  ex-pw  28123  indifundif  30200  iuninc  30228  difico  30420  esum2dlem  31238  fiunelcarsg  31461  carsgclctunlem1  31462  carsggect  31463  bnj601  32079  bnj1416  32196  subfacp1lem1  32311  cvmliftlem10  32426  satf0  32504  frrlem14  33021  noextend  33058  noextendseq  33059  nosupbday  33090  nosupbnd1  33099  nosupbnd2  33101  noetalem2  33103  noetalem3  33104  noetalem4  33105  poimirlem4  34764  poimirlem18  34778  poimirlem21  34781  poimirlem22  34782  poimirlem25  34785  mbfresfi  34806  asindmre  34845  mapfzcons  39175  mapfzcons1  39176  diophin  39231  iocunico  39679  rp-fakeuninass  39744  rclexi  39837  rtrclex  39839  dfrtrcl5  39851  dfrcl2  39881  corcltrcl  39946  cotrclrcl  39949  frege109d  39964  frege131d  39971  fiiuncl  41189  cnrefiisp  41973  fourierdlem65  42319  fourierdlem89  42343  fourierdlem90  42344  fourierdlem91  42345  fourierdlem96  42350  fourierdlem97  42351  fourierdlem98  42352  fourierdlem99  42353  fourierdlem100  42354  fourierdlem105  42359  fourierdlem108  42362  fourierdlem109  42363  fourierdlem110  42364  fourierdlem112  42366  fourierdlem113  42367  isomenndlem  42675  hoidmvlelem3  42742  1fzopredsuc  43387  lmod1zr  44377
  Copyright terms: Public domain W3C validator