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

Theorem uneq12i 3327
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 3324 . 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 1623    u. cun 3150
This theorem is referenced by:  indir  3417  difundir  3422  difindi  3423  symdif1  3433  unrab  3439  rabun2  3447  dfif6  3568  dfif3  3575  dfif5  3577  unopab  4095  xpundi  4741  xpundir  4742  xpun  4747  dmun  4885  resundi  4969  resundir  4970  cnvun  5086  rnun  5089  imaundi  5093  imaundir  5094  dmtpop  5149  coundi  5174  coundir  5175  unidmrn  5202  dfdm2  5204  mptun  5374  resasplit  5411  fresaun  5412  fresaunres2  5413  fpr  5704  fvsnun2  5716  sbthlem5  6975  1sdom  7065  cdaassen  7808  hashgval  11340  hashinf  11342  vdwlem6  13033  setsres  13174  xpsc  13459  lefld  14348  opsrtoslem1  16225  volun  18902  iblcnlem1  19142  ex-dif  20810  ex-in  20812  ex-pw  20816  ex-xp  20823  ex-cnv  20824  ex-rn  20827  partfun  23240  sigaclfu2  23482  indval2  23598  subfacp1lem1  23710  subfacp1lem5  23715  predun  24190  symdif0  24368  symdifid  24370  fixun  24449  bpoly3  24793  onint1  24888  fldcnv  25056  dispos  25287  refssfne  26294  usgraexvlem  28127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157
  Copyright terms: Public domain W3C validator