Theorem uneq12i 4189

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

Syntax hints:   = wceq 1537   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  indir  4305  difundir  4310  difindi  4311  dfsymdif3  4325  unrab  4334  rabun2  4343  elnelun  4416  dfif6  4551  dfif3  4562  dfif5  4564  symdif0  5108  symdifid  5110  unopab  5248  xpundi  5768  xpundir  5769  xpun  5773  dmun  5935  resundi  6023  resundir  6024  cnvun  6174  rnun  6177  imaundi  6181  imaundir  6182  dmtpop  6249  coundi  6278  coundir  6279  unidmrn  6310  dfdm2  6312  predun  6360  mptun  6726  partfun  6727  resasplit  6791  fresaun  6792  fresaunres2  6793  residpr  7177  fpr  7188  sbthlem5  9153  1sdomOLD  9312  djuassen  10248  fz0to3un2pr  13686  fz0to4untppr  13687  fz0to5un2tp  13688  fzo0to42pr  13803  hashgval  14382  hashinf  14384  relexpcnv  15084  bpoly3  16106  vdwlem6  17033  setsres  17225  lefld  18662  opsrtoslem1  22102  volun  25599  nosupcbv  27765  noinfcbv  27780  lrold  27953  addsval2  28014  addscut  28029  addsunif  28053  addsbday  28068  mulsval2  28155  muls01  28156  mulsproplem2  28161  mulsproplem3  28162  mulsproplem4  28163  mulscut  28176  mulsunif  28194  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  mulsunif2  28214  precsexlemcbv  28248  onaddscl  28304  onmulscl  28305  n0scut  28356  1p1e2s  28418  nohalf  28425  ex-dif  30455  ex-in  30457  ex-pw  30461  ex-xp  30468  ex-cnv  30469  ex-rn  30472  fzodif1  32798  ordtprsuni  33865  indval2  33978  sigaclfu2  34085  eulerpartgbij  34337  subfacp1lem1  35147  subfacp1lem5  35152  fmla1  35355  fixun  35873  refssfne  36324  onint1  36415  bj-pr1un  36969  bj-pr21val  36979  bj-pr2un  36983  bj-pr22val  36985  poimirlem16  37596  poimirlem19  37599  itg2addnclem2  37632  iblabsnclem  37643  df3o3  43276  rclexi  43577  rtrclex  43579  cnvrcl0  43587  dfrtrcl5  43591  dfrcl2  43636  dfrcl4  43638  iunrelexp0  43664  relexpiidm  43666  corclrcl  43669  relexp01min  43675  corcltrcl  43701  cotrclrcl  43704  frege131d  43726  rnfdmpr  47196  31prm  47471