Theorem uneq12d 4156

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

Syntax hints:   → wi 4   = wceq 1533   ∪ cun 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-un 3945

This theorem is referenced by:  symdifeq1  4236  csbun  4430  csbprg  4705  disjpr2  4709  diftpsn3  4797  iunxprg  5089  relresdm1  6023  rnpropg  6211  suceq  6420  fntpg  6598  foun  6841  f1oprswap  6867  fnimapr  6965  xpprsng  7130  residpr  7133  fvsnun2  7173  fsnunfv  7177  fsnunres  7178  f1ofvswap  7296  xpord2pred  8125  xpord3pred  8132  frrlem12  8277  oarec  8557  ereq1  8705  mapunen  9141  cnfcomlem  9689  trcl  9718  djueq12  9894  r0weon  10002  infxpen  10004  cfsmolem  10260  cfsmo  10261  axdc3lem4  10443  ttukeylem3  10501  ttukey2g  10506  alephadd  10567  fpwwe2lem12  10632  wunex2  10728  wuncval2  10737  inar1  10765  prunioo  13454  fztp  13553  fzsuc2  13555  fseq1p1m1  13571  s3tpop  14856  s4dom  14866  trclun  14957  relexp0g  14965  relexpsucnnr  14968  dfrtrcl2  15005  setsvalg  17095  setsdm  17099  setsfun0  17101  setsid  17137  prdsval  17397  imasval  17453  mreexd  17582  mreexexlemd  17584  estrreslem2  18089  ipoval  18482  istsr  18535  gsumzaddlem  19826  pwssplit1  20892  psrval  21768  ordtval  23003  ordtcnv  23015  paste  23108  connsuba  23234  ptval2  23415  dfac14  23432  xkoptsub  23468  ptuncnv  23621  ptunhmeo  23622  xpstopnlem1  23623  alexsubALTlem3  23863  ustuqtop1  24056  rrxmvallem  25242  ovolioo  25407  uniiccdif  25417  itgsplitioo  25677  limcfval  25711  lhop2  25858  lgsquadlem2  27218  nodenselem5  27525  nosupbnd2lem1  27552  nosupbnd2  27553  noinfbnd2lem1  27567  noinfbnd2  27568  noetainflem2  27575  madeoldsuc  27715  lrold  27727  lrrecval  27760  addsval  27783  addsrid  27785  addscom  27787  addsproplem1  27790  addsprop  27797  addsass  27826  mulsval  27913  mulsrid  27917  mulsproplemcbv  27919  mulsproplem1  27920  mulsprop  27934  mulscom  27943  addsdi  27959  mulsass  27970  mulsunif2lem  27973  precsexlemcbv  28008  precsexlem3  28011  n0scut  28078  readdscl  28098  remulscl  28101  axlowdimlem13  28636  axlowdimlem15  28638  axlowdim  28643  eengv  28661  vtxdun  29162  trlsegvdeg  29904  numclwwlk3lem2lem  30060  ex-res  30118  imadifxp  32256  fnimatp  32326  cnvprop  32342  mptprop  32344  coprprop  32345  padct  32368  resf1o  32379  symgcom  32671  tocycfv  32695  tocycf  32703  tocyc01  32704  cycpm2tr  32705  cycpmco2f1  32710  cycpmco2rn  32711  cycpmconjv  32728  cycpmconjslem2  32741  idlsrgval  33048  rprmval  33064  zarclsun  33305  ordtprsval  33353  ordtprsuni  33354  ordtcnvNEW  33355  unelcarsg  33766  carsgclctunlem1  33771  eulerpartlemt  33825  sseqval  33842  probun  33873  bnj1373  34496  bnj1489  34522  cvmliftlem10  34740  satfvsuc  34807  satfdm  34815  satf0suc  34822  sat1el2xp  34825  fmlasuc0  34830  satffunlem1lem1  34848  satffunlem2lem1  34850  mrexval  34947  mrsubffval  34953  msrval  34984  mthmpps  35028  lineunray  35580  rdgssun  36715  exrecfnlem  36716  finixpnum  36929  ptrest  36943  poimirlem1  36945  poimirlem2  36946  poimirlem3  36947  poimirlem4  36948  poimirlem5  36949  poimirlem6  36950  poimirlem7  36951  poimirlem8  36952  poimirlem9  36953  poimirlem10  36954  poimirlem11  36955  poimirlem12  36956  poimirlem15  36959  poimirlem16  36960  poimirlem17  36961  poimirlem18  36962  poimirlem19  36963  poimirlem20  36964  poimirlem21  36965  poimirlem22  36966  poimirlem23  36967  poimirlem24  36968  poimirlem26  36970  poimirlem27  36971  poimirlem28  36972  poimirlem32  36976  mblfinlem2  36982  itg2addnclem2  36996  ldualset  38451  paddval  39125  paddcom  39140  dvafset  40331  dvaset  40332  dvhfset  40407  dvhset  40408  hdmapfval  41154  hlhilset  41261  metakunt17  41460  metakunt20  41463  metakunt21  41464  metakunt22  41465  metakunt24  41467  fsuppssindlem2  41619  istopclsd  41893  fzsplit1nn0  41947  diophrw  41952  eldioph2lem1  41953  eldioph2lem2  41954  diophin  41965  diophren  42006  pwssplit4  42286  mendval  42380  iocunico  42415  tfsconcatun  42542  tfsconcat0i  42550  onsucunitp  42578  oaun3  42587  rclexi  42821  rtrclex  42823  rtrclexi  42827  cnvrcl0  42831  dfrtrcl5  42835  dfrcl2  42880  dfrcl3  42881  iunrelexp0  42908  trclfvdecomr  42934  dfrtrcl4  42944  frege131d  42970  clsk3nimkb  43246  clsk1indlem3  43249  clsk1independent  43252  ntrclskb  43275  ntrclsk3  43276  ntrclsk13  43277  dvmptfprodlem  45111  caratheodorylem1  45693  ovnsubadd2lem  45812  ovolval4lem1  45816  fzopredsuc  46482  mndpsuppss  47202  aacllem  48002