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

Theorem uneq12i 3237
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 3234 . 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 3076
This theorem is referenced by:  indir  3324  difundir  3329  difindi  3330  symdif1  3340  unrab  3346  rabun2  3354  dfif6  3473  dfif3  3480  dfif5  3482  unopab  3992  xpundi  4648  xpundir  4649  xpun  4654  dmun  4792  resundi  4876  resundir  4877  cnvun  4993  rnun  4996  imaundi  5000  imaundir  5001  dmtpop  5055  coundi  5080  coundir  5081  unidmrn  5108  dfdm2  5110  mptun  5231  resasplit  5268  fresaun  5269  fresaunres2  5270  fpr  5556  fvsnun2  5568  sbthlem5  6860  1sdom  6950  cdaassen  7692  hashgval  11218  hashinf  11220  vdwlem6  12907  setsres  13048  xpsc  13333  lefld  14183  opsrtoslem1  16057  volun  18734  iblcnlem1  18974  ex-dif  20623  ex-in  20625  ex-pw  20629  ex-xp  20636  ex-cnv  20637  ex-rn  20640  subfacp1lem1  22881  subfacp1lem5  22886  predun  23358  symdif0  23543  symdifid  23545  fixun  23624  bpoly3  23967  onint1  24062  fldcnv  24221  dispos  24453  refssfne  25460
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083
  Copyright terms: Public domain W3C validator