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

Theorem uneq12i 3485
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 3482 . 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 1653    u. cun 3304
This theorem is referenced by:  indir  3574  difundir  3579  difindi  3580  symdif1  3591  unrab  3597  rabun2  3605  dfif6  3766  dfif3  3773  dfif5  3775  unopab  4309  xpundi  4959  xpundir  4960  xpun  4964  dmun  5105  resundi  5189  resundir  5190  cnvun  5306  rnun  5309  imaundi  5313  imaundir  5314  dmtpop  5375  coundi  5400  coundir  5401  unidmrn  5428  dfdm2  5430  mptun  5604  resasplit  5642  fresaun  5643  fresaunres2  5644  fpr  5943  fvsnun2  5958  sbthlem5  7250  1sdom  7340  cdaassen  8093  fzo0to42pr  11217  hashgval  11652  hashinf  11654  vdwlem6  13385  setsres  13526  xpsc  13813  lefld  14702  opsrtoslem1  16575  volun  19470  iblcnlem1  19708  usgraexvlem  21445  ex-dif  21762  ex-in  21764  ex-pw  21768  ex-xp  21775  ex-cnv  21776  ex-rn  21779  partfun  24118  indval2  24443  sigaclfu2  24535  subfacp1lem1  24896  subfacp1lem5  24901  predun  25496  symdif0  25700  symdifid  25702  fixun  25785  bpoly3  26135  onint1  26230  itg2addnclem2  26295  iblabsnclem  26306  refssfne  26412  rnfdmpr  28125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-un 3311
  Copyright terms: Public domain W3C validator