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

Theorem uneq12i 3513
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 3510 . 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 1369    u. cun 3331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-un 3338
This theorem is referenced by:  indir  3603  difundir  3608  difindi  3609  symdif1  3620  unrab  3626  rabun2  3634  dfif6  3799  dfif3  3808  dfif5  3810  unopab  4372  xpundi  4896  xpundir  4897  xpun  4901  dmun  5051  resundi  5129  resundir  5130  cnvun  5247  rnun  5250  imaundi  5254  imaundir  5255  dmtpop  5320  coundi  5344  coundir  5345  unidmrn  5372  dfdm2  5374  mptun  5546  resasplit  5586  fresaun  5587  fresaunres2  5588  residpr  5891  fpr  5895  fvsnun2  5919  sbthlem5  7430  1sdom  7520  cdaassen  8356  fzo0to42pr  11621  hashgval  12111  hashinf  12113  vdwlem6  14052  setsres  14207  xpsc  14500  lefld  15401  opsrtoslem1  17570  volun  21031  iblcnlem1  21270  usgraexvlem  23318  ex-dif  23635  ex-in  23637  ex-pw  23641  ex-xp  23648  ex-cnv  23649  ex-rn  23652  partfun  25998  ordtprsuni  26354  indval2  26476  sigaclfu2  26569  eulerpartgbij  26760  subfacp1lem1  27072  subfacp1lem5  27077  predun  27656  symdif0  27860  symdifid  27862  fixun  27945  bpoly3  28206  onint1  28300  itg2addnclem2  28449  iblabsnclem  28460  refssfne  28571  rnfdmpr  30154  bj-pr1un  32501  bj-pr21val  32511  bj-pr2un  32515  bj-pr22val  32517
  Copyright terms: Public domain W3C validator