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

Theorem uneq12 3482
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 3480 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uneq2 3481 . 2  |-  ( C  =  D  ->  ( B  u.  C )  =  ( B  u.  D ) )
31, 2sylan9eq 2494 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    u. cun 3304
This theorem is referenced by:  uneq12i  3485  uneq12d  3488  un00  3687  opthprc  4954  dmpropg  5372  unixp  5431  fntpg  5535  fnun  5580  resasplit  5642  fvun  5822  rankprb  7806  pm54.43  7918  xpscg  13814  ptuncnv  17870  evlseu  19968  sshjval  22883  diophun  26870  pwssplit4  27206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-un 3311
  Copyright terms: Public domain W3C validator