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

Step	Hyp	Ref	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 ) )
3	1, 2	sylan9eq 2528	1 |- ( ( A = B /\ C = D ) -> ( A u. C ) = ( B u. D ) )

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