Theorem uneq12i 4096

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

Syntax hints:   = wceq 1547   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888

This theorem is referenced by:  indir  4214  difundir  4219  difindi  4220  dfsymdif3  4234  unrab  4243  rabun2  4252  elnelun  4321  dfif6  4457  dfif3  4469  dfif5  4471  symdif0  5014  symdifid  5016  unopab  5152  xpundi  5687  xpundir  5688  xpun  5692  dmun  5852  resundi  5945  resundir  5946  cnvun  6093  rnun  6096  imaundi  6100  imaundir  6101  dmtpop  6169  coundi  6198  coundir  6199  unidmrn  6230  dfdm2  6232  predun  6279  mptun  6631  partfun  6632  resasplit  6697  fresaun  6698  fresaunres2  6699  residpr  7085  fpr  7097  sbthlem5  9019  djuassen  10092  indval2  12155  indconst0  12162  fz0to3un2pr  13574  fz0to4untppr  13575  fz0to5un2tp  13576  fzo0to42pr  13699  hashgval  14286  hashinf  14288  relexpcnv  14988  bpoly3  16014  vdwlem6  16948  setsres  17139  lefld  18549  opsrtoslem1  22031  volun  25530  nosupcbv  27684  noinfcbv  27699  lrold  27907  addsval2  27973  addcuts  27988  addsunif  28012  addbday  28028  mulsval2  28121  muls01  28122  mulsproplem2  28127  mulsproplem3  28128  mulsproplem4  28129  mulcut  28142  mulsunif  28160  addsdilem1  28161  addsdilem2  28162  mulsasslem1  28173  mulsasslem2  28174  mulsunif2  28180  precsexlemcbv  28216  onaddscl  28287  onmulscl  28288  n0cut  28344  twocut  28433  bdaypw2n0bndlem  28473  0reno  28506  1reno  28507  ex-dif  30511  ex-in  30513  ex-pw  30517  ex-xp  30524  ex-cnv  30525  ex-rn  30528  fzodif1  32884  ordtprsuni  34103  sigaclfu2  34305  eulerpartgbij  34556  subfacp1lem1  35407  subfacp1lem5  35412  fmla1  35615  fixun  36135  refssfne  36586  onint1  36677  ttcun  36740  bj-pr1un  37356  bj-pr21val  37366  bj-pr2un  37370  bj-pr22val  37372  poimirlem16  38003  poimirlem19  38006  itg2addnclem2  38039  iblabsnclem  38050  dfsucmap3  38830  redvmptabs  42837  df3o3  43759  rclexi  44059  rtrclex  44061  cnvrcl0  44069  dfrtrcl5  44073  dfrcl2  44118  dfrcl4  44120  iunrelexp0  44146  relexpiidm  44148  corclrcl  44151  relexp01min  44157  corcltrcl  44183  cotrclrcl  44186  frege131d  44208  rnfdmpr  47744  31prm  48075