Theorem uneq12d 4119

Description: Equality deduction for the union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Hypotheses

Ref	Expression
uneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
uneq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
uneq12d	⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Proof of Theorem uneq12d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		uneq12 4113	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907

This theorem is referenced by:  symdifeq1  4205  csbun  4391  csbprg  4662  disjpr2  4666  diftpsn3  4754  iunxprg  5044  relresdm1  5982  rnpropg  6169  suceqd  6373  fntpg  6541  foun  6781  f1oprswap  6807  fnimapr  6905  fnimatpd  6906  xpprsng  7073  residpr  7076  fvsnun2  7117  fsnunfv  7121  fsnunres  7122  f1ounsn  7206  f1ofvswap  7240  xpord2pred  8075  xpord3pred  8082  frrlem12  8227  oarec  8477  ereq1  8629  mapunen  9059  cnfcomlem  9589  trcl  9618  djueq12  9797  r0weon  9903  infxpen  9905  cfsmolem  10161  cfsmo  10162  axdc3lem4  10344  ttukeylem3  10402  ttukey2g  10407  alephadd  10468  fpwwe2lem12  10533  wunex2  10629  wuncval2  10638  inar1  10666  prunioo  13381  fztp  13480  fzsuc2  13482  fseq1p1m1  13498  s3tpop  14816  s4dom  14826  s2rn  14870  s3rn  14871  s7rn  14872  trclun  14921  relexp0g  14929  relexpsucnnr  14932  dfrtrcl2  14969  setsvalg  17077  setsdm  17081  setsfun0  17083  setsid  17118  prdsval  17359  imasval  17415  mreexd  17548  mreexexlemd  17550  estrreslem2  18044  ipoval  18436  istsr  18489  mndpsuppss  18673  gsumzaddlem  19834  pwssplit1  20994  psrval  21853  psdmullem  22081  ordtval  23105  ordtcnv  23117  paste  23210  connsuba  23336  ptval2  23517  dfac14  23534  xkoptsub  23570  ptuncnv  23723  ptunhmeo  23724  xpstopnlem1  23725  alexsubALTlem3  23965  ustuqtop1  24157  rrxmvallem  25332  ovolioo  25497  uniiccdif  25507  itgsplitioo  25767  limcfval  25801  lhop2  25948  lgsquadlem2  27320  nodenselem5  27628  nosupbnd2lem1  27655  nosupbnd2  27656  noinfbnd2lem1  27670  noinfbnd2  27671  noetainflem2  27678  madeoldsuc  27831  lrold  27843  lrrecval  27883  addsval  27906  addsrid  27908  addscom  27910  addsproplem1  27913  addsprop  27920  addsass  27949  mulsval  28049  mulsrid  28053  mulsproplemcbv  28055  mulsproplem1  28056  mulsprop  28070  mulscom  28079  addsdi  28095  mulsass  28106  mulsunif2lem  28109  precsexlemcbv  28145  precsexlem3  28148  n0scut  28263  halfcut  28379  pw2cut2  28383  readdscl  28402  remulscl  28405  axlowdimlem13  28933  axlowdimlem15  28935  axlowdim  28940  eengv  28958  vtxdun  29461  trlsegvdeg  30205  numclwwlk3lem2lem  30361  ex-res  30419  imadifxp  32579  suppun2  32663  cnvprop  32675  mptprop  32677  coprprop  32678  fmptunsnop  32679  padct  32699  resf1o  32711  symgcom  33050  tocycfv  33076  tocycf  33084  tocyc01  33085  cycpm2tr  33086  cycpmco2f1  33091  cycpmco2rn  33092  cycpmconjv  33109  cycpmconjslem2  33122  elrgspnlem4  33210  rlocval  33224  idlsrgval  33466  rprmval  33479  zarclsun  33881  ordtprsval  33929  ordtprsuni  33930  ordtcnvNEW  33931  unelcarsg  34323  carsgclctunlem1  34328  eulerpartlemt  34382  sseqval  34399  probun  34430  bnj1373  35040  bnj1489  35066  cvmliftlem10  35336  satfvsuc  35403  satfdm  35411  satf0suc  35418  sat1el2xp  35421  fmlasuc0  35426  satffunlem1lem1  35444  satffunlem2lem1  35446  mrexval  35543  mrsubffval  35549  msrval  35580  mthmpps  35624  lineunray  36187  rdgssun  37418  exrecfnlem  37419  finixpnum  37651  ptrest  37665  poimirlem1  37667  poimirlem2  37668  poimirlem3  37669  poimirlem4  37670  poimirlem5  37671  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem9  37675  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem18  37684  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem23  37689  poimirlem24  37690  poimirlem26  37692  poimirlem27  37693  poimirlem28  37694  poimirlem32  37698  mblfinlem2  37704  itg2addnclem2  37718  ldualset  39170  paddval  39843  paddcom  39858  dvafset  41049  dvaset  41050  dvhfset  41125  dvhset  41126  hdmapfval  41872  hlhilset  41979  dvun  42398  fsuppssindlem2  42631  istopclsd  42739  fzsplit1nn0  42793  diophrw  42798  eldioph2lem1  42799  eldioph2lem2  42800  diophin  42811  diophren  42852  pwssplit4  43128  mendval  43218  iocunico  43250  tfsconcatun  43376  tfsconcat0i  43384  onsucunitp  43412  oaun3  43421  rclexi  43654  rtrclex  43656  rtrclexi  43660  cnvrcl0  43664  dfrtrcl5  43668  dfrcl2  43713  dfrcl3  43714  iunrelexp0  43741  trclfvdecomr  43767  dfrtrcl4  43777  frege131d  43803  clsk3nimkb  44079  clsk1indlem3  44082  clsk1independent  44085  ntrclskb  44108  ntrclsk3  44109  ntrclsk13  44110  permaxinf2lem  45051  dvmptfprodlem  45988  caratheodorylem1  46570  ovnsubadd2lem  46689  ovolval4lem1  46693  fzopredsuc  47360  clnbgrval  47859  cycl3grtri  47984  aacllem  49839