Theorem uneq12i 4118

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

Syntax hints:   = wceq 1541   ∪ cun 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  indir  4238  difundir  4243  difindi  4244  dfsymdif3  4258  unrab  4267  rabun2  4276  elnelun  4345  dfif6  4482  dfif3  4494  dfif5  4496  symdif0  5040  symdifid  5042  unopab  5178  xpundi  5693  xpundir  5694  xpun  5698  dmun  5859  resundi  5952  resundir  5953  cnvun  6100  rnun  6103  imaundi  6107  imaundir  6108  dmtpop  6176  coundi  6205  coundir  6206  unidmrn  6237  dfdm2  6239  predun  6286  mptun  6638  partfun  6639  resasplit  6704  fresaun  6705  fresaunres2  6706  residpr  7088  fpr  7099  sbthlem5  9019  djuassen  10089  fz0to3un2pr  13545  fz0to4untppr  13546  fz0to5un2tp  13547  fzo0to42pr  13669  hashgval  14256  hashinf  14258  relexpcnv  14958  bpoly3  15981  vdwlem6  16914  setsres  17105  lefld  18515  opsrtoslem1  22010  volun  25502  nosupcbv  27670  noinfcbv  27685  lrold  27893  addsval2  27959  addcuts  27974  addsunif  27998  addbday  28014  mulsval2  28107  muls01  28108  mulsproplem2  28113  mulsproplem3  28114  mulsproplem4  28115  mulcut  28128  mulsunif  28146  addsdilem1  28147  addsdilem2  28148  mulsasslem1  28159  mulsasslem2  28160  mulsunif2  28166  precsexlemcbv  28202  onaddscl  28273  onmulscl  28274  n0cut  28330  twocut  28419  bdaypw2n0bndlem  28459  0reno  28492  1reno  28493  ex-dif  30498  ex-in  30500  ex-pw  30504  ex-xp  30511  ex-cnv  30512  ex-rn  30515  fzodif1  32872  indval2  32933  indconst0  32939  ordtprsuni  34076  sigaclfu2  34278  eulerpartgbij  34529  subfacp1lem1  35373  subfacp1lem5  35378  fmla1  35581  fixun  36101  refssfne  36552  onint1  36643  bj-pr1un  37204  bj-pr21val  37214  bj-pr2un  37218  bj-pr22val  37220  poimirlem16  37837  poimirlem19  37840  itg2addnclem2  37873  iblabsnclem  37884  dfsucmap3  38647  redvmptabs  42625  df3o3  43566  rclexi  43866  rtrclex  43868  cnvrcl0  43876  dfrtrcl5  43880  dfrcl2  43925  dfrcl4  43927  iunrelexp0  43953  relexpiidm  43955  corclrcl  43958  relexp01min  43964  corcltrcl  43990  cotrclrcl  43993  frege131d  44015  rnfdmpr  47537  31prm  47853