Theorem uneq12i 3727

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

Hypotheses

Ref	Expression
uneq1i.1	⊢ 𝐴 = 𝐵
uneq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
uneq12i	⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)

Proof of Theorem uneq12i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		uneq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		uneq12 3724	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	mp2an 704	1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)

Syntax hints:   = wceq 1475   ∪ cun 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545

This theorem is referenced by:  indir  3834  difundir  3839  difindi  3840  dfsymdif3  3852  unrab  3857  rabun2  3865  elnelun  3918  dfif6  4039  dfif3  4050  dfif5  4052  symdif0  4533  symdifid  4535  unopab  4660  xpundi  5094  xpundir  5095  xpun  5099  dmun  5253  resundi  5330  resundir  5331  cnvun  5457  rnun  5460  imaundi  5464  imaundir  5465  dmtpop  5529  coundi  5553  coundir  5554  unidmrn  5582  dfdm2  5584  predun  5621  mptun  5938  resasplit  5987  fresaun  5988  fresaunres2  5989  residpr  6315  fpr  6326  fvsnun2  6354  sbthlem5  7959  1sdom  8048  cdaassen  8887  fz0to3un2pr  12310  fz0to4untppr  12311  fzo0to42pr  12422  hashgval  12982  hashinf  12984  relexpcnv  13623  bpoly3  14628  vdwlem6  15528  setsres  15729  xpsc  16040  lefld  17049  opsrtoslem1  19305  volun  23120  iblcnlem1  23360  ex-dif  26672  ex-in  26674  ex-pw  26678  ex-xp  26685  ex-cnv  26686  ex-rn  26689  partfun  28858  ordtprsuni  29293  indval2  29404  sigaclfu2  29511  eulerpartgbij  29761  subfacp1lem1  30415  subfacp1lem5  30420  fixun  31186  refssfne  31523  onint1  31618  bj-pr1un  32184  bj-pr21val  32194  bj-pr2un  32198  bj-pr22val  32200  poimirlem16  32595  poimirlem19  32598  itg2addnclem2  32632  iblabsnclem  32643  rclexi  36941  rtrclex  36943  cnvrcl0  36951  dfrtrcl5  36955  dfrcl2  36985  dfrcl4  36987  iunrelexp0  37013  relexpiidm  37015  corclrcl  37018  relexp01min  37024  corcltrcl  37050  cotrclrcl  37053  frege131d  37075  df3o3  37343  31prm  40050  rnfdmpr  40325