Theorem uneq12 3616

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1370   u. cun 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-un 3444

This theorem is referenced by:  uneq12i  3619  uneq12d  3622  un00  3825  opthprc  4997  dmpropg  5423  unixp  5481  fntpg  5584  fnun  5628  resasplit  5692  fvun  5873  rankprb  8173  pm54.43  8285  xpscg  14619  evlseu  17736  ptuncnv  19522  sshjval  24932  diophun  29283  pwssplit4  29613  bj-2upleq  32862