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

Theorem uneq12i 3328
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 3325 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3mp2an 655 1  |-  ( A  u.  C )  =  ( B  u.  D
)
Colors of variables: wff set class
Syntax hints:    = wceq 1624    u. cun 3151
This theorem is referenced by:  indir  3418  difundir  3423  difindi  3424  symdif1  3434  unrab  3440  rabun2  3448  dfif6  3569  dfif3  3576  dfif5  3578  unopab  4096  xpundi  4740  xpundir  4741  xpun  4746  dmun  4884  resundi  4968  resundir  4969  cnvun  5085  rnun  5088  imaundi  5092  imaundir  5093  dmtpop  5147  coundi  5172  coundir  5173  unidmrn  5200  dfdm2  5202  mptun  5339  resasplit  5376  fresaun  5377  fresaunres2  5378  fpr  5665  fvsnun2  5677  sbthlem5  6970  1sdom  7060  cdaassen  7803  hashgval  11334  hashinf  11336  vdwlem6  13027  setsres  13168  xpsc  13453  lefld  14342  opsrtoslem1  16219  volun  18896  iblcnlem1  19136  ex-dif  20785  ex-in  20787  ex-pw  20791  ex-xp  20798  ex-cnv  20799  ex-rn  20802  subfacp1lem1  23114  subfacp1lem5  23119  predun  23591  symdif0  23776  symdifid  23778  fixun  23857  bpoly3  24200  onint1  24295  fldcnv  24454  dispos  24686  refssfne  25693
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158
  Copyright terms: Public domain W3C validator