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

Theorem uneq12i 3556
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 3553 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3mp2an 676 1  |-  ( A  u.  C )  =  ( B  u.  D
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    u. cun 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-v 3019  df-un 3379
This theorem is referenced by:  indir  3659  difundir  3664  difindi  3665  dfsymdif3  3676  symdif1OLD  3677  unrab  3682  rabun2  3690  elnelun  3726  dfif6  3852  dfif3  3863  dfif5  3865  symdif0  4314  symdifid  4316  unopab  4437  xpundi  4844  xpundir  4845  xpun  4849  dmun  4998  resundi  5075  resundir  5076  cnvun  5198  rnun  5201  imaundi  5205  imaundir  5206  dmtpop  5269  coundi  5293  coundir  5294  unidmrn  5323  dfdm2  5325  predun  5361  mptun  5665  resasplit  5708  fresaun  5709  fresaunres2  5710  residpr  6022  fpr  6026  fvsnun2  6054  sbthlem5  7634  1sdom  7723  cdaassen  8558  fzo0to42pr  11945  hashgval  12463  hashinf  12465  relexpcnv  13037  bpoly3  14049  vdwlem6  14874  setsres  15089  xpsc  15401  lefld  16410  opsrtoslem1  18645  volun  22435  iblcnlem1  22682  usgraexmplvtxlem  25059  ex-dif  25810  ex-in  25812  ex-pw  25816  ex-xp  25823  ex-cnv  25824  ex-rn  25827  partfun  28219  ordtprsuni  28672  indval2  28783  sigaclfu2  28890  eulerpartgbij  29152  subfacp1lem1  29849  subfacp1lem5  29854  fixun  30620  refssfne  30958  onint1  31053  bj-pr1un  31508  bj-pr21val  31518  bj-pr2un  31522  bj-pr22val  31524  poimirlem16  31863  poimirlem19  31866  itg2addnclem2  31901  iblabsnclem  31912  rclexi  36135  rtrclex  36137  cnvrcl0  36145  dfrtrcl5  36149  dfrcl2  36179  dfrcl4  36181  iunrelexp0  36207  relexpiidm  36209  corclrcl  36212  relexp01min  36218  corcltrcl  36244  cotrclrcl  36247  frege131d  36269  rnfdmpr  38821
  Copyright terms: Public domain W3C validator