Theorem uneq12i 3417

Description: Equality inference for union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
uneq1i.1	⊢ A = B
uneq12i.2	⊢ C = D

Assertion

Ref	Expression
uneq12i	⊢ (A ∪ C) = (B ∪ D)

Proof of Theorem uneq12i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2 ⊢ A = B
2		uneq12i.2	. 2 ⊢ C = D
3		uneq12 3414	. 2 ⊢ ((A = B ∧ C = D) → (A ∪ C) = (B ∪ D))
4	1, 2, 3	mp2an 653	1 ⊢ (A ∪ C) = (B ∪ D)

Syntax hints:   = wceq 1642   ∪ cun 3208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-un 3215

This theorem is referenced by:  indir  3504  difundir  3509  difindi  3510  symdif1  3520  unrab  3527  rabun2  3535  dfun4  3547  iunin  3548  dfif6  3666  dfif3  3673  dfif5  3675  nnc0suc  4413  nnsucelrlem3  4427  ltfintrilem1  4466  dfop2  4576  phiun  4615  opeq  4620  unopab  4639  xpundi  4833  xpundir  4834  xpun  4835  resundi  4982  resundir  4983  cnvun  5034  rnun  5037  imaundi  5040  imaundir  5041  dmtpop  5072  coundi  5083  coundir  5084  fpr  5438  fvsnun2  5449  clos1basesuc  5883  ce2  6193  sbthlem1  6204