Theorem uneq12i 3917

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

Syntax hints:   = wceq 1631   ∪ cun 3722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3729

This theorem is referenced by:  indir  4025  difundir  4030  difindi  4031  dfsymdif3  4042  unrab  4047  rabun2  4055  elnelun  4109  elnelunOLD  4111  dfif6  4229  dfif3  4240  dfif5  4242  symdif0  4732  symdifid  4734  unopab  4863  xpundi  5312  xpundir  5313  xpun  5317  dmun  5470  resundi  5552  resundir  5553  cnvun  5680  rnun  5683  imaundi  5687  imaundir  5688  dmtpop  5754  coundi  5781  coundir  5782  unidmrn  5810  dfdm2  5812  predun  5848  mptun  6166  resasplit  6215  fresaun  6216  fresaunres2  6217  residpr  6553  fpr  6565  fvsnun2  6594  sbthlem5  8231  1sdom  8320  cdaassen  9207  fz0to3un2pr  12650  fz0to4untppr  12651  fzo0to42pr  12764  hashgval  13325  hashinf  13327  relexpcnv  13984  bpoly3  14996  vdwlem6  15898  setsres  16109  xpsc  16426  lefld  17435  opsrtoslem1  19700  volun  23534  iblcnlem1  23775  ex-dif  27623  ex-in  27625  ex-pw  27629  ex-xp  27636  ex-cnv  27637  ex-rn  27640  partfun  29816  ordtprsuni  30306  indval2  30417  sigaclfu2  30525  eulerpartgbij  30775  subfacp1lem1  31500  subfacp1lem5  31505  fixun  32354  refssfne  32691  onint1  32786  bj-pr1un  33323  bj-pr21val  33333  bj-pr2un  33337  bj-pr22val  33339  poimirlem16  33759  poimirlem19  33762  itg2addnclem2  33795  iblabsnclem  33806  rclexi  38449  rtrclex  38451  cnvrcl0  38459  dfrtrcl5  38463  dfrcl2  38493  dfrcl4  38495  iunrelexp0  38521  relexpiidm  38523  corclrcl  38526  relexp01min  38532  corcltrcl  38558  cotrclrcl  38561  frege131d  38583  df3o3  38850  rnfdmpr  41824  31prm  42041