Theorem uneq12i 4168

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

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  indir  4234  difundir  4239  difindi  4240  dfsymdif3  4254  unrab  4263  rabun2  4272  elnelun  4346  dfif6  4488  dfif3  4500  dfif5  4502  symdif0  5050  symdifid  5052  unopab  5191  xpundi  5727  xpundir  5728  xpun  5732  dmun  5904  resundi  6000  resundir  6001  cnvun  6151  rnun  6154  imaundi  6159  imaundir  6160  dmtpop  6238  coundi  6267  coundir  6268  unidmrn  6306  dfdm2  6308  predun  6357  mptun  6715  partfun  6716  resasplit  6782  fresaun  6783  fresaunres2  6784  residpr  7178  fpr  7190  sbthlem5  9148  djuassen  10296  indval2  12365  indconst0  12372  fz0to3un2pr  13803  fz0to4untppr  13804  fz0to5un2tp  13805  fzo0to42pr  13928  hashgval  14518  hashinf  14520  relexpcnv  15231  bpoly3  16268  vdwlem6  17208  setsres  17400  lefld  18816  opsrtoslem1  22419  volun  25921  nosupcbv  28116  noinfcbv  28131  lrold  28340  addsval2  28406  addcuts  28421  addsunif  28445  addbday  28461  mulsval2  28554  muls01  28555  mulsproplem2  28560  mulsproplem3  28561  mulsproplem4  28562  mulcut  28575  mulsunif  28593  addsdilem1  28594  addsdilem2  28595  mulsasslem1  28606  mulsasslem2  28607  mulsunif2  28613  precsexlemcbv  28649  onaddscl  28720  onmulscl  28721  n0cut  28777  twocut  28866  bdaypw2n0bndlem  28906  0reno  28939  1reno  28940  ex-dif  31081  ex-in  31083  ex-pw  31087  ex-xp  31094  ex-cnv  31095  ex-rn  31098  fzodif1  33480  ordtprsuni  34662  sigaclfu2  34864  eulerpartgbij  35115  subfacp1lem1  36152  subfacp1lem5  36157  fmla1  36360  fixun  36886  refssfne  37361  onint1  37452  ttcun  37515  bj-pr1un  38131  bj-pr21val  38141  bj-pr2un  38145  bj-pr22val  38147  poimirlem16  38822  poimirlem19  38825  itg2addnclem2  38858  iblabsnclem  38869  dfproplem  38909  dfsucmap3  39661  redvmptabs  43677  df3o3  44577  rclexi  44876  rtrclex  44878  cnvrcl0  44886  dfrtrcl5  44890  dfrcl2  44935  dfrcl4  44937  iunrelexp0  44963  relexpiidm  44965  corclrcl  44968  relexp01min  44974  corcltrcl  45000  cotrclrcl  45003  frege131d  45025  rnfdmpr  48624  31prm  48955