Theorem uneq12i 4139

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

Syntax hints:   = wceq 1537   ∪ cun 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943

This theorem is referenced by:  indir  4254  difundir  4259  difindi  4260  dfsymdif3  4271  unrab  4276  rabun2  4284  elnelun  4345  dfif6  4472  dfif3  4483  dfif5  4485  symdif0  5009  symdifid  5011  unopab  5147  xpundi  5622  xpundir  5623  xpun  5627  dmun  5781  resundi  5869  resundir  5870  cnvun  6003  rnun  6006  imaundi  6010  imaundir  6011  dmtpop  6077  coundi  6102  coundir  6103  unidmrn  6132  dfdm2  6134  predun  6174  mptun  6496  resasplit  6550  fresaun  6551  fresaunres2  6552  residpr  6907  fpr  6918  sbthlem5  8633  1sdom  8723  djuassen  9606  fz0to3un2pr  13012  fz0to4untppr  13013  fzo0to42pr  13127  hashgval  13696  hashinf  13698  relexpcnv  14396  bpoly3  15414  vdwlem6  16324  setsres  16527  lefld  17838  opsrtoslem1  20266  volun  24148  ex-dif  28204  ex-in  28206  ex-pw  28210  ex-xp  28217  ex-cnv  28218  ex-rn  28221  partfun  30423  fzodif1  30518  ordtprsuni  31164  indval2  31275  sigaclfu2  31382  eulerpartgbij  31632  subfacp1lem1  32428  subfacp1lem5  32433  fmla1  32636  fixun  33372  refssfne  33708  onint1  33799  bj-pr1un  34317  bj-pr21val  34327  bj-pr2un  34331  bj-pr22val  34333  poimirlem16  34910  poimirlem19  34913  itg2addnclem2  34946  iblabsnclem  34957  rclexi  39982  rtrclex  39984  cnvrcl0  39992  dfrtrcl5  39996  dfrcl2  40026  dfrcl4  40028  iunrelexp0  40054  relexpiidm  40056  corclrcl  40059  relexp01min  40065  corcltrcl  40091  cotrclrcl  40094  frege131d  40116  df3o3  40382  rnfdmpr  43487  31prm  43767