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

Theorem uneq12i 3486
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 3483 . 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 1652    u. cun 3305
This theorem is referenced by:  indir  3576  difundir  3581  difindi  3582  symdif1  3593  unrab  3599  rabun2  3607  dfif6  3729  dfif3  3736  dfif5  3738  unopab  4271  xpundi  4916  xpundir  4917  xpun  4921  dmun  5062  resundi  5146  resundir  5147  cnvun  5263  rnun  5266  imaundi  5270  imaundir  5271  dmtpop  5332  coundi  5357  coundir  5358  unidmrn  5385  dfdm2  5387  mptun  5561  resasplit  5599  fresaun  5600  fresaunres2  5601  fpr  5900  fvsnun2  5915  sbthlem5  7207  1sdom  7297  cdaassen  8046  fzo0to42pr  11169  hashgval  11604  hashinf  11606  vdwlem6  13337  setsres  13478  xpsc  13765  lefld  14654  opsrtoslem1  16527  volun  19422  iblcnlem1  19662  usgraexvlem  21397  ex-dif  21714  ex-in  21716  ex-pw  21720  ex-xp  21727  ex-cnv  21728  ex-rn  21731  partfun  24070  indval2  24395  sigaclfu2  24487  subfacp1lem1  24848  subfacp1lem5  24853  predun  25440  symdif0  25618  symdifid  25620  fixun  25699  bpoly3  26047  onint1  26142  itg2addnclem2  26198  iblabsnclem  26209  refssfne  26306  rnfdmpr  28006
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-v 2945  df-un 3312
  Copyright terms: Public domain W3C validator