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

Theorem uneq12i 3652
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 3649 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3mp2an 672 1  |-  ( A  u.  C )  =  ( B  u.  D
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395    u. cun 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476
This theorem is referenced by:  indir  3753  difundir  3758  difindi  3759  dfsymdif3  3770  symdif1OLD  3771  unrab  3776  rabun2  3784  dfif6  3947  dfif3  3958  dfif5  3960  symdif0  4409  symdifid  4411  unopab  4532  xpundi  5061  xpundir  5062  xpun  5066  dmun  5219  resundi  5297  resundir  5298  cnvun  5418  rnun  5421  imaundi  5425  imaundir  5426  dmtpop  5490  coundi  5514  coundir  5515  unidmrn  5543  dfdm2  5545  mptun  5718  resasplit  5761  fresaun  5762  fresaunres2  5763  residpr  6076  fpr  6080  fvsnun2  6108  sbthlem5  7650  1sdom  7741  cdaassen  8579  fzo0to42pr  11904  hashgval  12411  hashinf  12413  vdwlem6  14516  setsres  14674  xpsc  14974  lefld  15983  opsrtoslem1  18275  volun  22081  iblcnlem1  22320  usgraexvlem  24522  ex-dif  25271  ex-in  25273  ex-pw  25277  ex-xp  25284  ex-cnv  25285  ex-rn  25288  partfun  27671  ordtprsuni  28062  indval2  28189  sigaclfu2  28294  eulerpartgbij  28508  subfacp1lem1  28820  subfacp1lem5  28825  predun  29466  fixun  29743  bpoly3  30004  onint1  30098  itg2addnclem2  30251  iblabsnclem  30262  refssfne  30360  rnfdmpr  32551  bj-pr1un  34683  bj-pr21val  34693  bj-pr2un  34697  bj-pr22val  34699
  Copyright terms: Public domain W3C validator