Theorem uneq12i 4160

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

Syntax hints:   = wceq 1533   ∪ cun 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3951

This theorem is referenced by:  indir  4276  difundir  4281  difindi  4282  dfsymdif3  4297  unrab  4306  rabun2  4315  elnelun  4393  dfif6  4535  dfif3  4546  dfif5  4548  symdif0  5092  symdifid  5094  unopab  5234  xpundi  5749  xpundir  5750  xpun  5754  dmun  5916  resundi  6002  resundir  6003  cnvun  6153  rnun  6156  imaundi  6160  imaundir  6161  dmtpop  6228  coundi  6257  coundir  6258  unidmrn  6289  dfdm2  6291  predun  6340  mptun  6706  partfun  6707  resasplit  6771  fresaun  6772  fresaunres2  6773  residpr  7156  fpr  7167  sbthlem5  9124  1sdomOLD  9286  djuassen  10217  fz0to3un2pr  13652  fz0to4untppr  13653  fzo0to42pr  13768  hashgval  14345  hashinf  14347  relexpcnv  15035  bpoly3  16055  vdwlem6  16983  setsres  17175  lefld  18612  opsrtoslem1  22060  volun  25557  nosupcbv  27724  noinfcbv  27739  lrold  27912  addsval2  27969  addscut  27984  addsunif  28008  mulsval2  28104  muls01  28105  mulsproplem2  28110  mulsproplem3  28111  mulsproplem4  28112  mulscut  28125  mulsunif  28143  addsdilem1  28144  addsdilem2  28145  mulsasslem1  28156  mulsasslem2  28157  mulsunif2  28163  precsexlemcbv  28197  n0scut  28298  ex-dif  30348  ex-in  30350  ex-pw  30354  ex-xp  30361  ex-cnv  30362  ex-rn  30365  fzodif1  32684  ordtprsuni  33702  indval2  33815  sigaclfu2  33922  eulerpartgbij  34174  subfacp1lem1  34971  subfacp1lem5  34976  fmla1  35179  fixun  35693  refssfne  36030  onint1  36121  bj-pr1un  36670  bj-pr21val  36680  bj-pr2un  36684  bj-pr22val  36686  poimirlem16  37297  poimirlem19  37300  itg2addnclem2  37333  iblabsnclem  37344  df3o3  42929  rclexi  43231  rtrclex  43233  cnvrcl0  43241  dfrtrcl5  43245  dfrcl2  43290  dfrcl4  43292  iunrelexp0  43318  relexpiidm  43320  corclrcl  43323  relexp01min  43329  corcltrcl  43355  cotrclrcl  43358  frege131d  43380  rnfdmpr  46843  31prm  47118