Theorem uneq12i 4167

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

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 4151

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-un 4153

This theorem is used by:  indir  4233  difundir  4238  difindi  4239  dfsymdif3  4253  unrab  4262  rabun2  4271  elnelun  4345  dfif6  4487  dfif3  4499  dfif5  4501  symdif0  5047  symdifid  5049  unopab  5187  xpundi  5723  xpundir  5724  xpun  5728  dmun  5896  resundi  5988  resundir  5989  cnvun  6138  rnun  6141  imaundi  6146  imaundir  6147  dmtpop  6225  coundi  6254  coundir  6255  unidmrn  6288  dfdm2  6290  predun  6337  mptun  6693  partfun  6694  resasplit  6760  fresaun  6761  fresaunres2  6762  residpr  7154  fpr  7166  sbthlem5  9121  djuassen  10267  indval2  12335  indconst0  12342  fz0to3un2pr  13773  fz0to4untppr  13774  fz0to5un2tp  13775  fzo0to42pr  13898  hashgval  14487  hashinf  14489  relexpcnv  15200  bpoly3  16236  vdwlem6  17176  setsres  17368  lefld  18778  opsrtoslem1  22376  volun  25878  nosupcbv  28071  noinfcbv  28086  lrold  28295  addsval2  28361  addcuts  28376  addsunif  28400  addbday  28416  mulsval2  28509  muls01  28510  mulsproplem2  28515  mulsproplem3  28516  mulsproplem4  28517  mulcut  28530  mulsunif  28548  addsdilem1  28549  addsdilem2  28550  mulsasslem1  28561  mulsasslem2  28562  mulsunif2  28568  precsexlemcbv  28604  onaddscl  28675  onmulscl  28676  n0cut  28732  twocut  28821  bdaypw2n0bndlem  28861  0reno  28894  1reno  28895  ex-dif  31036  ex-in  31038  ex-pw  31042  ex-xp  31049  ex-cnv  31050  ex-rn  31053  fzodif1  33437  ordtprsuni  34604  sigaclfu2  34806  eulerpartgbij  35057  subfacp1lem1  36065  subfacp1lem5  36070  fmla1  36273  fixun  36798  refssfne  37273  onint1  37364  ttcun  37427  bj-pr1un  38043  bj-pr21val  38053  bj-pr2un  38057  bj-pr22val  38059  poimirlem16  38694  poimirlem19  38697  itg2addnclem2  38730  iblabsnclem  38741  dfproplem  38781  dfsucmap3  39535  redvmptabs  43551  df3o3  44456  rclexi  44755  rtrclex  44757  cnvrcl0  44765  dfrtrcl5  44769  dfrcl2  44814  dfrcl4  44816  iunrelexp0  44842  relexpiidm  44844  corclrcl  44847  relexp01min  44853  corcltrcl  44879  cotrclrcl  44882  frege131d  44904  rnfdmpr  48490  31prm  48821