Theorem uneq12i 4120

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911

This theorem is used by:  indir  4239  difundir  4244  difindi  4245  dfsymdif3  4259  unrab  4268  rabun2  4277  elnelun  4350  dfif6  4492  dfif3  4504  dfif5  4506  symdif0  5053  symdifid  5055  unopab  5193  xpundi  5732  xpundir  5733  xpun  5737  dmun  5902  resundi  5994  resundir  5995  cnvun  6141  rnun  6144  imaundi  6149  imaundir  6150  dmtpop  6221  coundi  6250  coundir  6251  unidmrn  6284  dfdm2  6286  predun  6333  mptun  6685  partfun  6686  resasplit  6752  fresaun  6753  fresaunres2  6754  residpr  7145  fpr  7157  sbthlem5  9086  djuassen  10178  indval2  12240  indconst0  12247  fz0to3un2pr  13676  fz0to4untppr  13677  fz0to5un2tp  13678  fzo0to42pr  13801  hashgval  14389  hashinf  14391  relexpcnv  15098  bpoly3  16136  vdwlem6  17070  setsres  17262  lefld  18672  opsrtoslem1  22258  volun  25757  nosupcbv  27919  noinfcbv  27934  lrold  28143  addsval2  28209  addcuts  28224  addsunif  28248  addbday  28264  mulsval2  28357  muls01  28358  mulsproplem2  28363  mulsproplem3  28364  mulsproplem4  28365  mulcut  28378  mulsunif  28396  addsdilem1  28397  addsdilem2  28398  mulsasslem1  28409  mulsasslem2  28410  mulsunif2  28416  precsexlemcbv  28452  onaddscl  28523  onmulscl  28524  n0cut  28580  twocut  28669  bdaypw2n0bndlem  28709  0reno  28742  1reno  28743  ex-dif  30847  ex-in  30849  ex-pw  30853  ex-xp  30860  ex-cnv  30861  ex-rn  30864  fzodif1  33209  ordtprsuni  34375  sigaclfu2  34577  eulerpartgbij  34829  subfacp1lem1  35710  subfacp1lem5  35715  fmla1  35918  fixun  36438  refssfne  36928  onint1  37019  ttcun  37082  bj-pr1un  37698  bj-pr21val  37708  bj-pr2un  37712  bj-pr22val  37714  poimirlem16  38346  poimirlem19  38349  itg2addnclem2  38382  iblabsnclem  38393  dfsucmap3  39172  redvmptabs  43181  df3o3  44101  rclexi  44401  rtrclex  44403  cnvrcl0  44411  dfrtrcl5  44415  dfrcl2  44460  dfrcl4  44462  iunrelexp0  44488  relexpiidm  44490  corclrcl  44493  relexp01min  44499  corcltrcl  44525  cotrclrcl  44528  frege131d  44550  rnfdmpr  48078  31prm  48409