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  subfacp1lem1  23121  subfacp1lem5  23126  predun  23601  symdif0  23779  symdifid  23781  fixun  23860  bpoly3  24204  onint1  24299  fldcnv  24468  dispos  24699  refssfne  25706  usgraexvlem  27524
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