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

Theorem uneq12i 3340
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 3337 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3mp2an 653 1  |-  ( A  u.  C )  =  ( B  u.  D
)
Colors of variables: wff set class
Syntax hints:    = wceq 1632    u. cun 3163
This theorem is referenced by:  indir  3430  difundir  3435  difindi  3436  symdif1  3446  unrab  3452  rabun2  3460  dfif6  3581  dfif3  3588  dfif5  3590  unopab  4111  xpundi  4757  xpundir  4758  xpun  4763  dmun  4901  resundi  4985  resundir  4986  cnvun  5102  rnun  5105  imaundi  5109  imaundir  5110  dmtpop  5165  coundi  5190  coundir  5191  unidmrn  5218  dfdm2  5220  mptun  5390  resasplit  5427  fresaun  5428  fresaunres2  5429  fpr  5720  fvsnun2  5732  sbthlem5  6991  1sdom  7081  cdaassen  7824  hashgval  11356  hashinf  11358  vdwlem6  13049  setsres  13190  xpsc  13475  lefld  14364  opsrtoslem1  16241  volun  18918  iblcnlem1  19158  ex-dif  20826  ex-in  20828  ex-pw  20832  ex-xp  20839  ex-cnv  20840  ex-rn  20843  partfun  23255  sigaclfu2  23497  indval2  23613  subfacp1lem1  23725  subfacp1lem5  23730  predun  24261  symdif0  24439  symdifid  24441  fixun  24520  bpoly3  24865  onint1  24960  itg2addnclem2  25004  itgaddnclem2  25010  iblabsnclem  25014  fldcnv  25159  dispos  25390  refssfne  26397  fzo0to42pr  28211  usgraexvlem  28261
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170
  Copyright terms: Public domain W3C validator