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

Theorem uneq12i 3269
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 3266 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3mp2an 656 1  |-  ( A  u.  C )  =  ( B  u.  D
)
Colors of variables: wff set class
Syntax hints:    = wceq 1619    u. cun 3092
This theorem is referenced by:  indir  3359  difundir  3364  difindi  3365  symdif1  3375  unrab  3381  rabun2  3389  dfif6  3509  dfif3  3516  dfif5  3518  unopab  4035  xpundi  4694  xpundir  4695  xpun  4700  dmun  4838  resundi  4922  resundir  4923  cnvun  5039  rnun  5042  imaundi  5046  imaundir  5047  dmtpop  5101  coundi  5126  coundir  5127  unidmrn  5154  dfdm2  5156  mptun  5277  resasplit  5314  fresaun  5315  fresaunres2  5316  fpr  5603  fvsnun2  5615  sbthlem5  6908  1sdom  6998  cdaassen  7741  hashgval  11271  hashinf  11273  vdwlem6  12960  setsres  13101  xpsc  13386  lefld  14275  opsrtoslem1  16152  volun  18829  iblcnlem1  19069  ex-dif  20718  ex-in  20720  ex-pw  20724  ex-xp  20731  ex-cnv  20732  ex-rn  20735  subfacp1lem1  23047  subfacp1lem5  23052  predun  23524  symdif0  23709  symdifid  23711  fixun  23790  bpoly3  24133  onint1  24228  fldcnv  24387  dispos  24619  refssfne  25626
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-un 3099
  Copyright terms: Public domain W3C validator