Theorem uneq12d 4171

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  symdifeq1  4203  csbun  4402  csbprg  4670  disjpr2  4674  diftpsn3  4765  iunxprg  5059  relresdm1  6038  rnpropg  6237  suceqd  6451  fntpg  6625  foun  6868  f1oprswap  6896  fnimapr  6994  fnimatpd  6995  xpprsng  7169  xpsnprg  7170  xpsntpg  7171  residpr  7173  fvsnun2  7214  fsnunfv  7218  fsnunres  7219  f1ounsn  7306  f1ofvswap  7340  xpord2pred  8192  xpord3pred  8199  frrlem12  8346  oarec  8601  ereq1  8756  mapunen  9196  cnfcomlem  9730  trcl  9759  djueq12  10015  r0weon  10121  infxpen  10123  cfsmolem  10378  cfsmo  10379  axdc3lem4  10561  ttukeylem3  10619  ttukey2g  10624  alephadd  10692  fpwwe2lem12  10757  wunex2  10853  wuncval2  10862  inar1  10890  prunioo  13642  fztp  13744  fzsuc2  13746  fseq1p1m1  13762  s3tpop  15092  s4dom  15102  s2rn  15148  s3rn  15149  s7rn  15150  trclun  15199  relexp0g  15207  relexpsucnnr  15210  dfrtrcl2  15247  setsvalg  17376  setsdm  17380  setsfun0  17382  setsid  17417  prdsval  17658  imasval  17715  mreexd  17848  mreexexlemd  17850  estrreslem2  18344  ipoval  18736  istsr  18789  mndpsuppss  18991  gsumzaddlem  20168  pwssplit1  21367  psrval  22256  psdmullem  22519  ordtval  23540  ordtcnv  23552  paste  23645  connsuba  23771  ptval2  23953  dfac14  23970  xkoptsub  24006  ptuncnv  24159  ptunhmeo  24160  xpstopnlem1  24161  alexsubALTlem3  24401  ustuqtop1  24593  rrxmvallem  25758  ovolioo  25922  uniiccdif  25932  itgsplitioo  26191  limcfval  26225  lhop2  26368  lgsquadlem2  27741  nodenselem5  28078  nosupbnd2lem1  28105  nosupbnd2  28106  noinfbnd2lem1  28120  noinfbnd2  28121  noetainflem2  28128  madeoldsuc  28304  lrold  28316  lrrecval  28358  addsval  28381  addsrid  28383  addscom  28385  addsproplem1  28388  addsprop  28395  addsass  28424  mulsval  28528  mulsrid  28532  mulsproplemcbv  28534  mulsproplem1  28535  mulsprop  28549  mulscom  28558  addsdi  28574  mulsass  28585  mulsunif2lem  28588  precsexlemcbv  28625  precsexlem3  28628  n0cut  28753  halfcut  28877  pw2cut2  28881  readdscl  28918  remulscl  28921  axlowdimlem13  29565  axlowdimlem15  29567  axlowdim  29572  eengv  29590  vtxdun  30095  trlsegvdeg  30861  numclwwlk3lem2lem  31017  ex-res  31075  imadifxp  33270  fresunsn  33294  suppun2  33351  cnvprop  33363  mptprop  33365  coprprop  33366  fmptunsnop  33367  padct  33384  resf1o  33395  symgcom  33720  tocycfv  33746  tocycf  33754  tocyc01  33755  cycpm2tr  33756  cycpmco2f1  33761  cycpmco2rn  33762  cycpmconjv  33779  cycpmconjslem2  33792  elrgspnlem4  33882  rlocval  33896  idlsrgval  34119  rprmval  34132  extvfvcl  34251  zarclsun  34585  ordtprsval  34633  ordtprsuni  34634  ordtcnvNEW  34635  unelcarsg  35027  carsgclctunlem1  35032  eulerpartlemt  35086  sseqval  35103  probun  35134  bnj1373  35743  bnj1489  35769  brr0d  36014  cvmliftlem10  36239  satfvsuc  36306  satfdm  36314  satf0suc  36321  sat1el2xp  36324  fmlasuc0  36329  satffunlem1lem1  36347  satffunlem2lem1  36349  mrexval  36446  mrsubffval  36452  msrval  36483  mthmpps  36527  lineunray  37103  rdgssun  38506  exrecfnlem  38507  finixpnum  38733  ptrest  38742  poimirlem1  38744  poimirlem2  38745  poimirlem3  38746  poimirlem4  38747  poimirlem5  38748  poimirlem6  38749  poimirlem7  38750  poimirlem8  38751  poimirlem9  38752  poimirlem10  38753  poimirlem11  38754  poimirlem12  38755  poimirlem15  38758  poimirlem16  38759  poimirlem17  38760  poimirlem18  38761  poimirlem19  38762  poimirlem20  38763  poimirlem21  38764  poimirlem22  38765  poimirlem23  38766  poimirlem24  38767  poimirlem26  38769  poimirlem27  38770  poimirlem28  38771  poimirlem32  38775  mblfinlem2  38781  itg2addnclem2  38795  ecun  39528  ecuncnvepres  39530  ldualset  40385  paddval  41058  paddcom  41073  dvafset  42264  dvaset  42265  dvhfset  42340  dvhset  42341  hdmapfval  43087  hlhilset  43194  dvun  43614  fsuppssindlem2  43824  istopclsd  43915  fzsplit1nn0  43969  diophrw  43974  eldioph2lem1  43975  eldioph2lem2  43976  diophin  43987  diophren  44024  pwssplit4  44295  mendval  44384  iocunico  44416  tfsconcatun  44542  tfsconcat0i  44550  onsucunitp  44578  oaun3  44587  rclexi  44818  rtrclex  44820  rtrclexi  44824  cnvrcl0  44828  dfrtrcl5  44832  dfrcl2  44877  dfrcl3  44878  iunrelexp0  44905  trclfvdecomr  44931  dfrtrcl4  44941  frege131d  44967  clsk3nimkb  45243  clsk1indlem3  45246  clsk1independent  45249  ntrclskb  45272  ntrclsk3  45273  ntrclsk13  45274  permaxinf2lem  46208  dvmptfprodlem  47169  caratheodorylem1  47751  ovnsubadd2lem  47870  ovolval4lem1  47874  fzopredsuc  48609  clnbgrval  49135  cycl3grtri  49260  aacllem  51251