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 596	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907

This theorem is used by:  symdifeq1  4204  csbun  4402  csbprg  4673  disjpr2  4677  diftpsn3  4768  iunxprg  5060  relresdm1  6033  rnpropg  6222  suceqd  6429  fntpg  6597  foun  6840  f1oprswap  6867  fnimapr  6965  fnimatpd  6966  xpprsng  7139  xpsnprg  7140  xpsntpg  7141  residpr  7143  fvsnun2  7185  fsnunfv  7189  fsnunres  7190  f1ounsn  7277  f1ofvswap  7311  xpord2pred  8147  xpord3pred  8154  frrlem12  8300  oarec  8553  ereq1  8708  mapunen  9148  cnfcomlem  9682  trcl  9711  djueq12  9913  r0weon  10019  infxpen  10021  cfsmolem  10276  cfsmo  10277  axdc3lem4  10459  ttukeylem3  10517  ttukey2g  10522  alephadd  10590  fpwwe2lem12  10655  wunex2  10751  wuncval2  10760  inar1  10788  prunioo  13538  fztp  13639  fzsuc2  13641  fseq1p1m1  13657  s3tpop  14984  s4dom  14994  s2rn  15040  s3rn  15041  s7rn  15042  trclun  15091  relexp0g  15099  relexpsucnnr  15102  dfrtrcl2  15139  setsvalg  17264  setsdm  17268  setsfun0  17270  setsid  17305  prdsval  17546  imasval  17603  mreexd  17736  mreexexlemd  17738  estrreslem2  18232  ipoval  18624  istsr  18677  mndpsuppss  18878  gsumzaddlem  20054  pwssplit1  21249  psrval  22136  psdmullem  22399  ordtval  23420  ordtcnv  23432  paste  23525  connsuba  23651  ptval2  23833  dfac14  23850  xkoptsub  23886  ptuncnv  24039  ptunhmeo  24040  xpstopnlem1  24041  alexsubALTlem3  24281  ustuqtop1  24473  rrxmvallem  25638  ovolioo  25802  uniiccdif  25812  itgsplitioo  26072  limcfval  26106  lhop2  26249  lgsquadlem2  27625  nodenselem5  27932  nosupbnd2lem1  27959  nosupbnd2  27960  noinfbnd2lem1  27974  noinfbnd2  27975  noetainflem2  27982  madeoldsuc  28158  lrold  28170  lrrecval  28212  addsval  28235  addsrid  28237  addscom  28239  addsproplem1  28242  addsprop  28249  addsass  28278  mulsval  28382  mulsrid  28386  mulsproplemcbv  28388  mulsproplem1  28389  mulsprop  28403  mulscom  28412  addsdi  28428  mulsass  28439  mulsunif2lem  28442  precsexlemcbv  28479  precsexlem3  28482  n0cut  28607  halfcut  28731  pw2cut2  28735  readdscl  28772  remulscl  28775  axlowdimlem13  29419  axlowdimlem15  29421  axlowdim  29426  eengv  29444  vtxdun  29949  trlsegvdeg  30715  numclwwlk3lem2lem  30871  ex-res  30929  imadifxp  33082  fresunsn  33106  suppun2  33164  cnvprop  33176  mptprop  33178  coprprop  33179  fmptunsnop  33180  padct  33197  resf1o  33209  symgcom  33531  tocycfv  33557  tocycf  33565  tocyc01  33566  cycpm2tr  33567  cycpmco2f1  33572  cycpmco2rn  33573  cycpmconjv  33590  cycpmconjslem2  33603  elrgspnlem4  33693  rlocval  33707  idlsrgval  33921  rprmval  33934  extvfvcl  34054  zarclsun  34388  ordtprsval  34436  ordtprsuni  34437  ordtcnvNEW  34438  unelcarsg  34831  carsgclctunlem1  34836  eulerpartlemt  34890  sseqval  34907  probun  34938  bnj1373  35547  bnj1489  35573  cvmliftlem10  35881  satfvsuc  35948  satfdm  35956  satf0suc  35963  sat1el2xp  35966  fmlasuc0  35971  satffunlem1lem1  35989  satffunlem2lem1  35991  mrexval  36088  mrsubffval  36094  msrval  36125  mthmpps  36169  lineunray  36735  rdgssun  38140  exrecfnlem  38141  finixpnum  38367  ptrest  38376  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem5  38382  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem9  38386  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem18  38395  poimirlem19  38396  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem23  38400  poimirlem24  38401  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  poimirlem32  38409  mblfinlem2  38415  itg2addnclem2  38429  ecun  39149  ecuncnvepres  39151  ldualset  40006  paddval  40679  paddcom  40694  dvafset  41885  dvaset  41886  dvhfset  41961  dvhset  41962  hdmapfval  42708  hlhilset  42815  dvun  43242  fsuppssindlem2  43446  istopclsd  43553  fzsplit1nn0  43607  diophrw  43612  eldioph2lem1  43613  eldioph2lem2  43614  diophin  43625  diophren  43662  pwssplit4  43938  mendval  44028  iocunico  44060  tfsconcatun  44186  tfsconcat0i  44194  onsucunitp  44222  oaun3  44231  rclexi  44463  rtrclex  44465  rtrclexi  44469  cnvrcl0  44473  dfrtrcl5  44477  dfrcl2  44522  dfrcl3  44523  iunrelexp0  44550  trclfvdecomr  44576  dfrtrcl4  44586  frege131d  44612  clsk3nimkb  44888  clsk1indlem3  44891  clsk1independent  44894  ntrclskb  44917  ntrclsk3  44918  ntrclsk13  44919  permaxinf2lem  45843  dvmptfprodlem  46780  caratheodorylem1  47362  ovnsubadd2lem  47481  ovolval4lem1  47485  fzopredsuc  48220  clnbgrval  48746  cycl3grtri  48871  aacllem  50780