Theorem uneq12 3583

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 3581	. 2 |- ( A = B -> ( A u. C ) = ( B u. C ) )
2		uneq2 3582	. 2 |- ( C = D -> ( B u. C ) = ( B u. D ) )
3	1, 2	sylan9eq 2505	1 |- ( ( A = B /\ C = D ) -> ( A u. C ) = ( B u. D ) )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1444   u. cun 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-un 3409

This theorem is referenced by:  uneq12i  3586  uneq12d  3589  un00  3800  opthprc  4882  dmpropg  5309  unixp  5369  fntpg  5637  fnun  5682  resasplit  5753  fvun  5935  rankprb  8322  pm54.43  8434  xpscg  15464  evlseu  18739  ptuncnv  20822  sshjval  27003  bj-2upleq  31606  poimirlem4  31944  poimirlem9  31949  diophun  35616  pwssplit4  35947