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

Theorem uneq12 3658
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 3656 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uneq2 3657 . 2  |-  ( C  =  D  ->  ( B  u.  C )  =  ( B  u.  D ) )
31, 2sylan9eq 2528 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    u. cun 3479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-un 3486
This theorem is referenced by:  uneq12i  3661  uneq12d  3664  un00  3867  opthprc  5053  dmpropg  5487  unixp  5546  fntpg  5649  fnun  5693  resasplit  5761  fvun  5944  rankprb  8281  pm54.43  8393  xpscg  14830  evlseu  18055  ptuncnv  20176  sshjval  26091  diophun  30635  pwssplit4  30963  bj-2upleq  34052
  Copyright terms: Public domain W3C validator