Theorem uneq12d 4125

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 4119	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   = wceq 1563   ∪ cun 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912

This theorem is referenced by:  symdifeq1  4210  csbun  4398  csbprg  4671  disjpr2  4675  diftpsn3  4765  iunxprg  5058  relresdm1  6026  rnpropg  6213  suceqd  6417  fntpg  6585  foun  6829  f1oprswap  6856  fnimapr  6954  fnimatpd  6955  xpprsng  7126  residpr  7129  fvsnun2  7171  fsnunfv  7175  fsnunres  7176  f1ounsn  7260  f1ofvswap  7294  xpord2pred  8129  xpord3pred  8136  frrlem12  8282  oarec  8535  ereq1  8690  mapunen  9122  cnfcomlem  9656  trcl  9685  djueq12  9878  r0weon  9984  infxpen  9986  cfsmolem  10242  cfsmo  10243  axdc3lem4  10425  ttukeylem3  10483  ttukey2g  10488  alephadd  10550  fpwwe2lem12  10615  wunex2  10711  wuncval2  10720  inar1  10748  prunioo  13499  fztp  13599  fzsuc2  13601  fseq1p1m1  13617  s3tpop  14936  s4dom  14946  s2rn  14990  s3rn  14991  s7rn  14992  trclun  15041  relexp0g  15049  relexpsucnnr  15052  dfrtrcl2  15089  setsvalg  17216  setsdm  17220  setsfun0  17222  setsid  17257  prdsval  17498  imasval  17555  mreexd  17688  mreexexlemd  17690  estrreslem2  18184  ipoval  18576  istsr  18629  mndpsuppss  18813  gsumzaddlem  19982  pwssplit1  21149  psrval  22025  psdmullem  22288  ordtval  23307  ordtcnv  23319  paste  23412  connsuba  23538  ptval2  23719  dfac14  23736  xkoptsub  23772  ptuncnv  23925  ptunhmeo  23926  xpstopnlem1  23927  alexsubALTlem3  24167  ustuqtop1  24359  rrxmvallem  25524  ovolioo  25688  uniiccdif  25698  itgsplitioo  25958  limcfval  25992  lhop2  26135  lgsquadlem2  27503  nodenselem5  27810  nosupbnd2lem1  27837  nosupbnd2  27838  noinfbnd2lem1  27852  noinfbnd2  27853  noetainflem2  27860  madeoldsuc  28036  lrold  28048  lrrecval  28090  addsval  28113  addsrid  28115  addscom  28117  addsproplem1  28120  addsprop  28127  addsass  28156  mulsval  28260  mulsrid  28264  mulsproplemcbv  28266  mulsproplem1  28267  mulsprop  28281  mulscom  28290  addsdi  28306  mulsass  28317  mulsunif2lem  28320  precsexlemcbv  28357  precsexlem3  28360  n0cut  28485  halfcut  28609  pw2cut2  28613  readdscl  28650  remulscl  28653  axlowdimlem13  29213  axlowdimlem15  29215  axlowdim  29220  eengv  29238  vtxdun  29740  trlsegvdeg  30487  numclwwlk3lem2lem  30643  ex-res  30701  imadifxp  32856  fresunsn  32882  suppun2  32941  cnvprop  32953  mptprop  32955  coprprop  32956  fmptunsnop  32957  padct  32975  resf1o  32987  symgcom  33316  tocycfv  33342  tocycf  33350  tocyc01  33351  cycpm2tr  33352  cycpmco2f1  33357  cycpmco2rn  33358  cycpmconjv  33375  cycpmconjslem2  33388  elrgspnlem4  33478  rlocval  33492  idlsrgval  33710  rprmval  33723  extvfvcl  33843  zarclsun  34177  ordtprsval  34225  ordtprsuni  34226  ordtcnvNEW  34227  unelcarsg  34619  carsgclctunlem1  34624  eulerpartlemt  34678  sseqval  34695  probun  34726  bnj1373  35335  bnj1489  35361  cvmliftlem10  35657  satfvsuc  35724  satfdm  35732  satf0suc  35739  sat1el2xp  35742  fmlasuc0  35747  satffunlem1lem1  35765  satffunlem2lem1  35767  mrexval  35864  mrsubffval  35870  msrval  35901  mthmpps  35945  lineunray  36510  rdgssun  37884  exrecfnlem  37885  finixpnum  38116  ptrest  38130  poimirlem1  38132  poimirlem2  38133  poimirlem3  38134  poimirlem4  38135  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem9  38140  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem23  38154  poimirlem24  38155  poimirlem26  38157  poimirlem27  38158  poimirlem28  38159  poimirlem32  38163  mblfinlem2  38169  itg2addnclem2  38183  ecun  38904  ecuncnvepres  38906  ldualset  39761  paddval  40434  paddcom  40449  dvafset  41640  dvaset  41641  dvhfset  41716  dvhset  41717  hdmapfval  42463  hlhilset  42570  dvun  42980  fsuppssindlem2  43186  istopclsd  43293  fzsplit1nn0  43347  diophrw  43352  eldioph2lem1  43353  eldioph2lem2  43354  diophin  43365  diophren  43402  pwssplit4  43678  mendval  43768  iocunico  43800  tfsconcatun  43926  tfsconcat0i  43934  onsucunitp  43962  oaun3  43971  rclexi  44203  rtrclex  44205  rtrclexi  44209  cnvrcl0  44213  dfrtrcl5  44217  dfrcl2  44262  dfrcl3  44263  iunrelexp0  44290  trclfvdecomr  44316  dfrtrcl4  44326  frege131d  44352  clsk3nimkb  44628  clsk1indlem3  44631  clsk1independent  44634  ntrclskb  44657  ntrclsk3  44658  ntrclsk13  44659  permaxinf2lem  45586  dvmptfprodlem  46516  caratheodorylem1  47098  ovnsubadd2lem  47217  ovolval4lem1  47221  fzopredsuc  47916  clnbgrval  48442  cycl3grtri  48567  aacllem  50430