Theorem uneq12 3591

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

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1405   u. cun 3411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-un 3418

This theorem is referenced by:  uneq12i  3594  uneq12d  3597  un00  3804  opthprc  4870  dmpropg  5296  unixp  5356  fntpg  5623  fnun  5667  resasplit  5737  fvun  5918  rankprb  8300  pm54.43  8412  xpscg  15170  evlseu  18503  ptuncnv  20598  sshjval  26668  bj-2upleq  31122  diophun  35048  pwssplit4  35377