Theorem uneq12i 4088

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

Syntax hints:   = wceq 1538   ∪ cun 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886

This theorem is referenced by:  indir  4202  difundir  4207  difindi  4208  dfsymdif3  4221  unrab  4226  rabun2  4234  elnelun  4297  dfif6  4428  dfif3  4439  dfif5  4441  symdif0  4970  symdifid  4972  unopab  5109  xpundi  5584  xpundir  5585  xpun  5589  dmun  5743  resundi  5832  resundir  5833  cnvun  5968  rnun  5971  imaundi  5975  imaundir  5976  dmtpop  6042  coundi  6067  coundir  6068  unidmrn  6098  dfdm2  6100  predun  6140  mptun  6466  partfun  6467  resasplit  6522  fresaun  6523  fresaunres2  6524  residpr  6882  fpr  6893  sbthlem5  8615  1sdom  8705  djuassen  9589  fz0to3un2pr  13004  fz0to4untppr  13005  fzo0to42pr  13119  hashgval  13689  hashinf  13691  relexpcnv  14386  bpoly3  15404  vdwlem6  16312  setsres  16517  lefld  17828  opsrtoslem1  20723  volun  24149  ex-dif  28208  ex-in  28210  ex-pw  28214  ex-xp  28221  ex-cnv  28222  ex-rn  28225  fzodif1  30542  ordtprsuni  31272  indval2  31383  sigaclfu2  31490  eulerpartgbij  31740  subfacp1lem1  32539  subfacp1lem5  32544  fmla1  32747  fixun  33483  refssfne  33819  onint1  33910  bj-pr1un  34439  bj-pr21val  34449  bj-pr2un  34453  bj-pr22val  34455  poimirlem16  35073  poimirlem19  35076  itg2addnclem2  35109  iblabsnclem  35120  rclexi  40315  rtrclex  40317  cnvrcl0  40325  dfrtrcl5  40329  dfrcl2  40375  dfrcl4  40377  iunrelexp0  40403  relexpiidm  40405  corclrcl  40408  relexp01min  40414  corcltrcl  40440  cotrclrcl  40443  frege131d  40465  df3o3  40728  rnfdmpr  43837  31prm  44114