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

Theorem uneq12i 3597
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 3594 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3mp2an 683 1  |-  ( A  u.  C )  =  ( B  u.  D
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1454    u. cun 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-un 3420
This theorem is referenced by:  indir  3702  difundir  3707  difindi  3708  dfsymdif3  3719  symdif1OLD  3720  unrab  3725  rabun2  3733  elnelun  3769  dfif6  3895  dfif3  3906  dfif5  3908  symdif0  4368  symdifid  4370  unopab  4491  xpundi  4905  xpundir  4906  xpun  4910  dmun  5059  resundi  5136  resundir  5137  cnvun  5259  rnun  5262  imaundi  5266  imaundir  5267  dmtpop  5330  coundi  5354  coundir  5355  unidmrn  5384  dfdm2  5386  predun  5422  mptun  5730  resasplit  5775  fresaun  5776  fresaunres2  5777  residpr  6091  fpr  6095  fvsnun2  6123  sbthlem5  7711  1sdom  7800  cdaassen  8637  fz0to3un2pr  11922  fzo0to42pr  12030  hashgval  12549  hashinf  12551  relexpcnv  13146  bpoly3  14159  vdwlem6  14984  setsres  15199  xpsc  15511  lefld  16520  opsrtoslem1  18755  volun  22546  iblcnlem1  22793  usgraexmplvtxlem  25170  ex-dif  25921  ex-in  25923  ex-pw  25927  ex-xp  25934  ex-cnv  25935  ex-rn  25938  partfun  28326  ordtprsuni  28773  indval2  28884  sigaclfu2  28991  eulerpartgbij  29253  subfacp1lem1  29950  subfacp1lem5  29955  fixun  30724  refssfne  31062  onint1  31157  bj-pr1un  31641  bj-pr21val  31651  bj-pr2un  31655  bj-pr22val  31657  poimirlem16  32000  poimirlem19  32003  itg2addnclem2  32038  iblabsnclem  32049  rclexi  36266  rtrclex  36268  cnvrcl0  36276  dfrtrcl5  36280  dfrcl2  36310  dfrcl4  36312  iunrelexp0  36338  relexpiidm  36340  corclrcl  36343  relexp01min  36349  corcltrcl  36375  cotrclrcl  36378  frege131d  36400  rnfdmpr  39056
  Copyright terms: Public domain W3C validator