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

Theorem uneq12 3266
Description: Equality theorem for union of two classes. (Contributed by NM, 29-Mar-1998.)
Assertion
Ref Expression
uneq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )

Proof of Theorem uneq12
StepHypRef Expression
1 uneq1 3264 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uneq2 3265 . 2  |-  ( C  =  D  ->  ( B  u.  C )  =  ( B  u.  D ) )
31, 2sylan9eq 2308 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1619    u. cun 3092
This theorem is referenced by:  uneq12i  3269  uneq12d  3272  un00  3432  opthprc  4689  dmpropg  5098  unixp  5157  fnun  5253  resasplit  5314  fvun  5488  rankprb  7456  pm54.43  7566  xpscg  13387  ptuncnv  17425  evlseu  19327  sshjval  21854  hdrmp  25038  diophun  26185  pwssplit4  26523
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