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

Theorem uneq12i 3288
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 3285 . 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 3111
This theorem is referenced by:  indir  3378  difundir  3383  difindi  3384  symdif1  3394  unrab  3400  rabun2  3408  dfif6  3528  dfif3  3535  dfif5  3537  unopab  4055  xpundi  4715  xpundir  4716  xpun  4721  dmun  4859  resundi  4943  resundir  4944  cnvun  5060  rnun  5063  imaundi  5067  imaundir  5068  dmtpop  5122  coundi  5147  coundir  5148  unidmrn  5175  dfdm2  5177  mptun  5298  resasplit  5335  fresaun  5336  fresaunres2  5337  fpr  5624  fvsnun2  5636  sbthlem5  6929  1sdom  7019  cdaassen  7762  hashgval  11292  hashinf  11294  vdwlem6  12981  setsres  13122  xpsc  13407  lefld  14296  opsrtoslem1  16173  volun  18850  iblcnlem1  19090  ex-dif  20739  ex-in  20741  ex-pw  20745  ex-xp  20752  ex-cnv  20753  ex-rn  20756  subfacp1lem1  23068  subfacp1lem5  23073  predun  23545  symdif0  23730  symdifid  23732  fixun  23811  bpoly3  24154  onint1  24249  fldcnv  24408  dispos  24640  refssfne  25647
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 2759  df-un 3118
  Copyright terms: Public domain W3C validator