Theorem uneq12i 4119

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

Syntax hints:   = wceq 1560   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909

This theorem is referenced by:  indir  4238  difundir  4243  difindi  4244  dfsymdif3  4258  unrab  4267  rabun2  4276  elnelun  4347  dfif6  4483  dfif3  4495  dfif5  4497  symdif0  5042  symdifid  5044  unopab  5180  xpundi  5716  xpundir  5717  xpun  5721  dmun  5886  resundi  5979  resundir  5980  cnvun  6126  rnun  6129  imaundi  6134  imaundir  6135  dmtpop  6205  coundi  6234  coundir  6235  unidmrn  6266  dfdm2  6268  predun  6315  mptun  6667  partfun  6668  resasplit  6734  fresaun  6735  fresaunres2  6736  residpr  7125  fpr  7137  sbthlem5  9063  djuassen  10135  indval2  12200  indconst0  12207  fz0to3un2pr  13634  fz0to4untppr  13635  fz0to5un2tp  13636  fzo0to42pr  13759  hashgval  14346  hashinf  14348  relexpcnv  15048  bpoly3  16088  vdwlem6  17022  setsres  17214  lefld  18624  opsrtoslem1  22108  volun  25607  nosupcbv  27766  noinfcbv  27781  lrold  27990  addsval2  28056  addcuts  28071  addsunif  28095  addbday  28111  mulsval2  28204  muls01  28205  mulsproplem2  28210  mulsproplem3  28211  mulsproplem4  28212  mulcut  28225  mulsunif  28243  addsdilem1  28244  addsdilem2  28245  mulsasslem1  28256  mulsasslem2  28257  mulsunif2  28263  precsexlemcbv  28299  onaddscl  28370  onmulscl  28371  n0cut  28427  twocut  28516  bdaypw2n0bndlem  28556  0reno  28589  1reno  28590  ex-dif  30625  ex-in  30627  ex-pw  30631  ex-xp  30638  ex-cnv  30639  ex-rn  30642  fzodif1  32994  ordtprsuni  34216  sigaclfu2  34418  eulerpartgbij  34669  subfacp1lem1  35529  subfacp1lem5  35534  fmla1  35737  fixun  36257  refssfne  36718  onint1  36809  ttcun  36872  bj-pr1un  37488  bj-pr21val  37498  bj-pr2un  37502  bj-pr22val  37504  poimirlem16  38135  poimirlem19  38138  itg2addnclem2  38171  iblabsnclem  38182  dfsucmap3  38962  redvmptabs  42969  df3o3  43891  rclexi  44191  rtrclex  44193  cnvrcl0  44201  dfrtrcl5  44205  dfrcl2  44250  dfrcl4  44252  iunrelexp0  44278  relexpiidm  44280  corclrcl  44283  relexp01min  44289  corcltrcl  44315  cotrclrcl  44318  frege131d  44340  rnfdmpr  47875  31prm  48206