Theorem uneq12i 4141

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

Syntax hints:   = wceq 1540   ∪ cun 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931

This theorem is referenced by:  indir  4261  difundir  4266  difindi  4267  dfsymdif3  4281  unrab  4290  rabun2  4299  elnelun  4368  dfif6  4503  dfif3  4515  dfif5  4517  symdif0  5061  symdifid  5063  unopab  5200  xpundi  5723  xpundir  5724  xpun  5728  dmun  5890  resundi  5980  resundir  5981  cnvun  6131  rnun  6134  imaundi  6138  imaundir  6139  dmtpop  6207  coundi  6236  coundir  6237  unidmrn  6268  dfdm2  6270  predun  6317  mptun  6684  partfun  6685  resasplit  6748  fresaun  6749  fresaunres2  6750  residpr  7133  fpr  7144  sbthlem5  9101  1sdomOLD  9257  djuassen  10193  fz0to3un2pr  13646  fz0to4untppr  13647  fz0to5un2tp  13648  fzo0to42pr  13769  hashgval  14351  hashinf  14353  relexpcnv  15054  bpoly3  16074  vdwlem6  17006  setsres  17197  lefld  18602  opsrtoslem1  22013  volun  25498  nosupcbv  27666  noinfcbv  27681  lrold  27860  addsval2  27922  addscut  27937  addsunif  27961  addsbday  27976  mulsval2  28066  muls01  28067  mulsproplem2  28072  mulsproplem3  28073  mulsproplem4  28074  mulscut  28087  mulsunif  28105  addsdilem1  28106  addsdilem2  28107  mulsasslem1  28118  mulsasslem2  28119  mulsunif2  28125  precsexlemcbv  28160  onaddscl  28226  onmulscl  28227  n0scut  28278  1p1e2s  28354  twocut  28361  ex-dif  30404  ex-in  30406  ex-pw  30410  ex-xp  30417  ex-cnv  30418  ex-rn  30421  fzodif1  32769  indval2  32831  ordtprsuni  33950  sigaclfu2  34152  eulerpartgbij  34404  subfacp1lem1  35201  subfacp1lem5  35206  fmla1  35409  fixun  35927  refssfne  36376  onint1  36467  bj-pr1un  37021  bj-pr21val  37031  bj-pr2un  37035  bj-pr22val  37037  poimirlem16  37660  poimirlem19  37663  itg2addnclem2  37696  iblabsnclem  37707  redvmptabs  42403  df3o3  43338  rclexi  43639  rtrclex  43641  cnvrcl0  43649  dfrtrcl5  43653  dfrcl2  43698  dfrcl4  43700  iunrelexp0  43726  relexpiidm  43728  corclrcl  43731  relexp01min  43737  corcltrcl  43763  cotrclrcl  43766  frege131d  43788  rnfdmpr  47310  31prm  47611