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

Theorem uneq12i 3624
Description: Equality inference for union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
uneq1i.1  |-  A  =  B
uneq12i.2  |-  C  =  D
Assertion
Ref Expression
uneq12i  |-  ( A  u.  C )  =  ( B  u.  D
)

Proof of Theorem uneq12i
StepHypRef Expression
1 uneq1i.1 . 2  |-  A  =  B
2 uneq12i.2 . 2  |-  C  =  D
3 uneq12 3621 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3mp2an 676 1  |-  ( A  u.  C )  =  ( B  u.  D
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    u. cun 3440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447
This theorem is referenced by:  indir  3727  difundir  3732  difindi  3733  dfsymdif3  3744  symdif1OLD  3745  unrab  3750  rabun2  3758  dfif6  3918  dfif3  3929  dfif5  3931  symdif0  4379  symdifid  4381  unopab  4501  xpundi  4907  xpundir  4908  xpun  4912  dmun  5061  resundi  5138  resundir  5139  cnvun  5261  rnun  5264  imaundi  5268  imaundir  5269  dmtpop  5332  coundi  5356  coundir  5357  unidmrn  5386  dfdm2  5388  predun  5423  mptun  5727  resasplit  5770  fresaun  5771  fresaunres2  5772  residpr  6083  fpr  6087  fvsnun2  6115  sbthlem5  7692  1sdom  7781  cdaassen  8610  fzo0to42pr  11997  hashgval  12515  hashinf  12517  relexpcnv  13077  bpoly3  14089  vdwlem6  14899  setsres  15114  xpsc  15414  lefld  16423  opsrtoslem1  18642  volun  22375  iblcnlem1  22622  usgraexvlem  24968  ex-dif  25718  ex-in  25720  ex-pw  25724  ex-xp  25731  ex-cnv  25732  ex-rn  25735  partfun  28118  ordtprsuni  28564  indval2  28675  sigaclfu2  28782  eulerpartgbij  29031  subfacp1lem1  29690  subfacp1lem5  29695  fixun  30461  refssfne  30799  onint1  30894  bj-pr1un  31346  bj-pr21val  31356  bj-pr2un  31360  bj-pr22val  31362  poimirlem16  31660  poimirlem19  31663  itg2addnclem2  31698  iblabsnclem  31709  dfrcl2  35905  dfrcl4  35907  iunrelexp0  35933  relexpiidm  35935  corclrcl  35938  relexp01min  35944  corcltrcl  35970  cotrclrcl  35973  frege131d  35995  rnfdmpr  38385
  Copyright terms: Public domain W3C validator