Theorem uneq12i 3993

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

Syntax hints:   = wceq 1658   ∪ cun 3797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-v 3417  df-un 3804

This theorem is referenced by:  indir  4106  difundir  4111  difindi  4112  dfsymdif3  4123  unrab  4128  rabun2  4136  elnelun  4192  dfif6  4310  dfif3  4321  dfif5  4323  symdif0  4818  symdifid  4820  unopab  4952  xpundi  5405  xpundir  5406  xpun  5410  dmun  5564  resundi  5648  resundir  5649  cnvun  5780  rnun  5783  imaundi  5787  imaundir  5788  dmtpop  5853  coundi  5878  coundir  5879  unidmrn  5907  dfdm2  5909  predun  5945  mptun  6259  resasplit  6312  fresaun  6313  fresaunres2  6314  residpr  6660  fpr  6673  fvsnun2OLD  6706  sbthlem5  8344  1sdom  8433  cdaassen  9320  fz0to3un2pr  12737  fz0to4untppr  12738  fzo0to42pr  12851  hashgval  13414  hashinf  13416  relexpcnv  14153  bpoly3  15162  vdwlem6  16062  setsres  16265  xpsc  16571  lefld  17580  opsrtoslem1  19845  volun  23712  iblcnlem1  23954  ex-dif  27839  ex-in  27841  ex-pw  27845  ex-xp  27852  ex-cnv  27853  ex-rn  27856  partfun  30024  ordtprsuni  30511  indval2  30622  sigaclfu2  30730  eulerpartgbij  30980  subfacp1lem1  31708  subfacp1lem5  31713  fixun  32556  refssfne  32892  onint1  32982  bj-pr1un  33514  bj-pr21val  33524  bj-pr2un  33528  bj-pr22val  33530  poimirlem16  33970  poimirlem19  33973  itg2addnclem2  34006  iblabsnclem  34017  rclexi  38764  rtrclex  38766  cnvrcl0  38774  dfrtrcl5  38778  dfrcl2  38808  dfrcl4  38810  iunrelexp0  38836  relexpiidm  38838  corclrcl  38841  relexp01min  38847  corcltrcl  38873  cotrclrcl  38876  frege131d  38898  df3o3  39164  rnfdmpr  42185  31prm  42343