Theorem uneq12i 4132

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 4129	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)

Syntax hints:   = wceq 1540   ∪ cun 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922

This theorem is referenced by:  indir  4252  difundir  4257  difindi  4258  dfsymdif3  4272  unrab  4281  rabun2  4290  elnelun  4359  dfif6  4494  dfif3  4506  dfif5  4508  symdif0  5052  symdifid  5054  unopab  5190  xpundi  5710  xpundir  5711  xpun  5715  dmun  5877  resundi  5967  resundir  5968  cnvun  6118  rnun  6121  imaundi  6125  imaundir  6126  dmtpop  6194  coundi  6223  coundir  6224  unidmrn  6255  dfdm2  6257  predun  6304  mptun  6667  partfun  6668  resasplit  6733  fresaun  6734  fresaunres2  6735  residpr  7118  fpr  7129  sbthlem5  9061  1sdomOLD  9203  djuassen  10139  fz0to3un2pr  13597  fz0to4untppr  13598  fz0to5un2tp  13599  fzo0to42pr  13721  hashgval  14305  hashinf  14307  relexpcnv  15008  bpoly3  16031  vdwlem6  16964  setsres  17155  lefld  18558  opsrtoslem1  21969  volun  25453  nosupcbv  27621  noinfcbv  27636  lrold  27815  addsval2  27877  addscut  27892  addsunif  27916  addsbday  27931  mulsval2  28021  muls01  28022  mulsproplem2  28027  mulsproplem3  28028  mulsproplem4  28029  mulscut  28042  mulsunif  28060  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  mulsunif2  28080  precsexlemcbv  28115  onaddscl  28181  onmulscl  28182  n0scut  28233  1p1e2s  28309  twocut  28316  ex-dif  30359  ex-in  30361  ex-pw  30365  ex-xp  30372  ex-cnv  30373  ex-rn  30376  fzodif1  32722  indval2  32784  ordtprsuni  33916  sigaclfu2  34118  eulerpartgbij  34370  subfacp1lem1  35173  subfacp1lem5  35178  fmla1  35381  fixun  35904  refssfne  36353  onint1  36444  bj-pr1un  36998  bj-pr21val  37008  bj-pr2un  37012  bj-pr22val  37014  poimirlem16  37637  poimirlem19  37640  itg2addnclem2  37673  iblabsnclem  37684  redvmptabs  42355  df3o3  43310  rclexi  43611  rtrclex  43613  cnvrcl0  43621  dfrtrcl5  43625  dfrcl2  43670  dfrcl4  43672  iunrelexp0  43698  relexpiidm  43700  corclrcl  43703  relexp01min  43709  corcltrcl  43735  cotrclrcl  43738  frege131d  43760  rnfdmpr  47286  31prm  47602