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

Theorem uneq12i 3459
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 3456 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3mp2an 654 1  |-  ( A  u.  C )  =  ( B  u.  D
)
Colors of variables: wff set class
Syntax hints:    = wceq 1649    u. cun 3278
This theorem is referenced by:  indir  3549  difundir  3554  difindi  3555  symdif1  3566  unrab  3572  rabun2  3580  dfif6  3702  dfif3  3709  dfif5  3711  unopab  4244  xpundi  4889  xpundir  4890  xpun  4894  dmun  5035  resundi  5119  resundir  5120  cnvun  5236  rnun  5239  imaundi  5243  imaundir  5244  dmtpop  5305  coundi  5330  coundir  5331  unidmrn  5358  dfdm2  5360  mptun  5534  resasplit  5572  fresaun  5573  fresaunres2  5574  fpr  5873  fvsnun2  5888  sbthlem5  7180  1sdom  7270  cdaassen  8018  fzo0to42pr  11141  hashgval  11576  hashinf  11578  vdwlem6  13309  setsres  13450  xpsc  13737  lefld  14626  opsrtoslem1  16499  volun  19392  iblcnlem1  19632  usgraexvlem  21367  ex-dif  21684  ex-in  21686  ex-pw  21690  ex-xp  21697  ex-cnv  21698  ex-rn  21701  partfun  24040  indval2  24365  sigaclfu2  24457  subfacp1lem1  24818  subfacp1lem5  24823  predun  25404  symdif0  25582  symdifid  25584  fixun  25663  bpoly3  26008  onint1  26103  itg2addnclem2  26156  iblabsnclem  26167  refssfne  26264  rnfdmpr  27964
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285
  Copyright terms: Public domain W3C validator