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

Theorem uneq12 3483
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 3481 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uneq2 3482 . 2  |-  ( C  =  D  ->  ( B  u.  C )  =  ( B  u.  D ) )
31, 2sylan9eq 2482 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    u. cun 3305
This theorem is referenced by:  uneq12i  3486  uneq12d  3489  un00  3650  opthprc  4911  dmpropg  5329  unixp  5388  fntpg  5492  fnun  5537  resasplit  5599  fvun  5779  rankprb  7761  pm54.43  7871  xpscg  13766  ptuncnv  17822  evlseu  19920  sshjval  22835  diophun  26764  pwssplit4  27101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-v 2945  df-un 3312
  Copyright terms: Public domain W3C validator