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

Theorem uneq12 3234
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 3232 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uneq2 3233 . 2  |-  ( C  =  D  ->  ( B  u.  C )  =  ( B  u.  D ) )
31, 2sylan9eq 2305 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 3076
This theorem is referenced by:  uneq12i  3237  uneq12d  3240  un00  3397  opthprc  4643  dmpropg  5052  unixp  5111  fnun  5207  resasplit  5268  fvun  5441  rankprb  7407  pm54.43  7517  xpscg  13334  ptuncnv  17330  evlseu  19232  sshjval  21759  hdrmp  24872  diophun  26019  pwssplit4  26357
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