Theorem uneq12i 3988

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

Syntax hints:   = wceq 1601   ∪ cun 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-un 3797

This theorem is referenced by:  indir  4102  difundir  4107  difindi  4108  dfsymdif3  4119  unrab  4124  rabun2  4132  elnelun  4192  dfif6  4310  dfif3  4321  dfif5  4323  symdif0  4832  symdifid  4834  unopab  4966  xpundi  5419  xpundir  5420  xpun  5424  dmun  5578  resundi  5662  resundir  5663  cnvun  5794  rnun  5797  imaundi  5801  imaundir  5802  dmtpop  5867  coundi  5892  coundir  5893  unidmrn  5921  dfdm2  5923  predun  5959  mptun  6273  resasplit  6326  fresaun  6327  fresaunres2  6328  residpr  6676  fpr  6689  fvsnun2OLD  6722  sbthlem5  8364  1sdom  8453  cdaassen  9341  fz0to3un2pr  12764  fz0to4untppr  12765  fzo0to42pr  12878  hashgval  13442  hashinf  13444  relexpcnv  14186  bpoly3  15195  vdwlem6  16098  setsres  16301  xpsc  16607  lefld  17616  opsrtoslem1  19884  volun  23753  iblcnlem1  23995  ex-dif  27859  ex-in  27861  ex-pw  27865  ex-xp  27872  ex-cnv  27873  ex-rn  27876  partfun  30045  ordtprsuni  30567  indval2  30678  sigaclfu2  30786  eulerpartgbij  31036  subfacp1lem1  31764  subfacp1lem5  31769  fixun  32609  refssfne  32945  onint1  33035  bj-pr1un  33567  bj-pr21val  33577  bj-pr2un  33581  bj-pr22val  33583  poimirlem16  34056  poimirlem19  34059  itg2addnclem2  34092  iblabsnclem  34103  rclexi  38889  rtrclex  38891  cnvrcl0  38899  dfrtrcl5  38903  dfrcl2  38933  dfrcl4  38935  iunrelexp0  38961  relexpiidm  38963  corclrcl  38966  relexp01min  38972  corcltrcl  38998  cotrclrcl  39001  frege131d  39023  df3o3  39289  rnfdmpr  42332  31prm  42543