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

Theorem uneq12i 3656
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 3653 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3mp2an 672 1  |-  ( A  u.  C )  =  ( B  u.  D
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    u. cun 3474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481
This theorem is referenced by:  indir  3746  difundir  3751  difindi  3752  symdif1  3763  unrab  3769  rabun2  3777  dfif6  3942  dfif3  3953  dfif5  3955  unopab  4522  xpundi  5052  xpundir  5053  xpun  5057  dmun  5209  resundi  5287  resundir  5288  cnvun  5411  rnun  5414  imaundi  5418  imaundir  5419  dmtpop  5484  coundi  5508  coundir  5509  unidmrn  5537  dfdm2  5539  mptun  5712  resasplit  5755  fresaun  5756  fresaunres2  5757  residpr  6065  fpr  6069  fvsnun2  6097  sbthlem5  7631  1sdom  7722  cdaassen  8562  fzo0to42pr  11869  hashgval  12376  hashinf  12378  vdwlem6  14363  setsres  14518  xpsc  14812  lefld  15713  opsrtoslem1  17947  volun  21718  iblcnlem1  21957  usgraexvlem  24099  ex-dif  24849  ex-in  24851  ex-pw  24855  ex-xp  24862  ex-cnv  24863  ex-rn  24866  partfun  27216  ordtprsuni  27565  indval2  27696  sigaclfu2  27789  eulerpartgbij  27979  subfacp1lem1  28291  subfacp1lem5  28296  predun  28875  symdif0  29079  symdifid  29081  fixun  29164  bpoly3  29425  onint1  29519  itg2addnclem2  29672  iblabsnclem  29683  refssfne  29794  rnfdmpr  31803  bj-pr1un  33660  bj-pr21val  33670  bj-pr2un  33674  bj-pr22val  33676
  Copyright terms: Public domain W3C validator