Theorem uneq12d 4104

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

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-un 3897

This theorem is referenced by:  symdifeq1  4184  csbun  4378  csbprg  4649  disjpr2  4653  diftpsn3  4741  iunxprg  5032  rnpropg  6140  suceq  6346  fntpg  6523  foun  6764  f1oprswap  6790  fnimapr  6884  xpprsng  7044  residpr  7047  fvsnun2  7087  fsnunfv  7091  fsnunres  7092  f1ofvswap  7210  frrlem12  8144  oarec  8424  ereq1  8536  mapunen  8971  cnfcomlem  9501  trcl  9530  djueq12  9706  r0weon  9814  infxpen  9816  cfsmolem  10072  cfsmo  10073  axdc3lem4  10255  ttukeylem3  10313  ttukey2g  10318  alephadd  10379  fpwwe2lem12  10444  wunex2  10540  wuncval2  10549  inar1  10577  prunioo  13259  fztp  13358  fzsuc2  13360  fseq1p1m1  13376  s3tpop  14667  s4dom  14677  trclun  14770  relexp0g  14778  relexpsucnnr  14781  dfrtrcl2  14818  setsvalg  16912  setsdm  16916  setsfun0  16918  setsid  16954  prdsval  17211  imasval  17267  mreexd  17396  mreexexlemd  17398  estrreslem2  17900  ipoval  18293  istsr  18346  gsumzaddlem  19567  pwssplit1  20366  psrval  21163  ordtval  22385  ordtcnv  22397  paste  22490  connsuba  22616  ptval2  22797  dfac14  22814  xkoptsub  22850  ptuncnv  23003  ptunhmeo  23004  xpstopnlem1  23005  alexsubALTlem3  23245  ustuqtop1  23438  rrxmvallem  24613  ovolioo  24777  uniiccdif  24787  itgsplitioo  25047  limcfval  25081  lhop2  25224  lgsquadlem2  26574  axlowdimlem13  27367  axlowdimlem15  27369  axlowdim  27374  eengv  27392  vtxdun  27893  trlsegvdeg  28636  numclwwlk3lem2lem  28792  ex-res  28850  imadifxp  30985  funresdm1  30989  fnimatp  31059  cnvprop  31074  mptprop  31076  coprprop  31077  padct  31099  resf1o  31110  symgcom  31397  tocycfv  31421  tocycf  31429  tocyc01  31430  cycpm2tr  31431  cycpmco2f1  31436  cycpmco2rn  31437  cycpmconjv  31454  cycpmconjslem2  31467  idlsrgval  31693  rprmval  31709  zarclsun  31865  ordtprsval  31913  ordtprsuni  31914  ordtcnvNEW  31915  unelcarsg  32324  carsgclctunlem1  32329  eulerpartlemt  32383  sseqval  32400  probun  32431  bnj1373  33055  bnj1489  33081  cvmliftlem10  33301  satfvsuc  33368  satfdm  33376  satf0suc  33383  sat1el2xp  33386  fmlasuc0  33391  satffunlem1lem1  33409  satffunlem2lem1  33411  mrexval  33508  mrsubffval  33514  msrval  33545  mthmpps  33589  xpord2pred  33837  xpord3pred  33843  nodenselem5  33936  nosupbnd2lem1  33963  nosupbnd2  33964  noinfbnd2lem1  33978  noinfbnd2  33979  noetainflem2  33986  madeoldsuc  34112  lrold  34122  lrrecval  34141  addsval  34171  addsid1  34172  addscom  34174  addscllem1  34176  lineunray  34494  rdgssun  35593  exrecfnlem  35594  finixpnum  35806  ptrest  35820  poimirlem1  35822  poimirlem2  35823  poimirlem3  35824  poimirlem4  35825  poimirlem5  35826  poimirlem6  35827  poimirlem7  35828  poimirlem8  35829  poimirlem9  35830  poimirlem10  35831  poimirlem11  35832  poimirlem12  35833  poimirlem15  35836  poimirlem16  35837  poimirlem17  35838  poimirlem18  35839  poimirlem19  35840  poimirlem20  35841  poimirlem21  35842  poimirlem22  35843  poimirlem23  35844  poimirlem24  35845  poimirlem26  35847  poimirlem27  35848  poimirlem28  35849  poimirlem32  35853  mblfinlem2  35859  itg2addnclem2  35873  ldualset  37181  paddval  37854  paddcom  37869  dvafset  39060  dvaset  39061  dvhfset  39136  dvhset  39137  hdmapfval  39883  hlhilset  39990  metakunt17  40183  metakunt20  40186  metakunt21  40187  metakunt22  40188  metakunt24  40190  fsuppssindlem2  40318  istopclsd  40559  fzsplit1nn0  40613  diophrw  40618  eldioph2lem1  40619  eldioph2lem2  40620  diophin  40631  diophren  40672  pwssplit4  40952  mendval  41046  iocunico  41080  rclexi  41261  rtrclex  41263  rtrclexi  41267  cnvrcl0  41271  dfrtrcl5  41275  dfrcl2  41320  dfrcl3  41321  iunrelexp0  41348  trclfvdecomr  41374  dfrtrcl4  41384  frege131d  41410  clsk3nimkb  41688  clsk1indlem3  41691  clsk1independent  41694  ntrclskb  41717  ntrclsk3  41718  ntrclsk13  41719  dvmptfprodlem  43534  caratheodorylem1  44114  ovnsubadd2lem  44233  ovolval4lem1  44237  fzopredsuc  44873  mndpsuppss  45765  aacllem  46563