Theorem uneq12d 4102

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896

This theorem is referenced by:  symdifeq1  4183  csbun  4377  csbprg  4650  disjpr2  4654  diftpsn3  4740  iunxprg  5029  rnpropg  6122  suceq  6328  fntpg  6490  foun  6730  f1oprswap  6755  fnimapr  6846  xpprsng  7006  residpr  7009  fvsnun2  7049  fsnunfv  7053  fsnunres  7054  f1ofvswap  7171  frrlem12  8097  oarec  8369  ereq1  8479  mapunen  8898  cnfcomlem  9418  trcl  9469  djueq12  9646  r0weon  9752  infxpen  9754  cfsmolem  10010  cfsmo  10011  axdc3lem4  10193  ttukeylem3  10251  ttukey2g  10256  alephadd  10317  fpwwe2lem12  10382  wunex2  10478  wuncval2  10487  inar1  10515  prunioo  13195  fztp  13294  fzsuc2  13296  fseq1p1m1  13312  s3tpop  14603  s4dom  14613  trclun  14706  relexp0g  14714  relexpsucnnr  14717  dfrtrcl2  14754  setsvalg  16848  setsdm  16852  setsfun0  16854  setsid  16890  prdsval  17147  imasval  17203  mreexd  17332  mreexexlemd  17334  estrreslem2  17836  ipoval  18229  istsr  18282  gsumzaddlem  19503  pwssplit1  20302  psrval  21099  ordtval  22321  ordtcnv  22333  paste  22426  connsuba  22552  ptval2  22733  dfac14  22750  xkoptsub  22786  ptuncnv  22939  ptunhmeo  22940  xpstopnlem1  22941  alexsubALTlem3  23181  ustuqtop1  23374  rrxmvallem  24549  ovolioo  24713  uniiccdif  24723  itgsplitioo  24983  limcfval  25017  lhop2  25160  lgsquadlem2  26510  axlowdimlem13  27303  axlowdimlem15  27305  axlowdim  27310  eengv  27328  vtxdun  27829  trlsegvdeg  28570  numclwwlk3lem2lem  28726  ex-res  28784  imadifxp  30919  funresdm1  30923  fnimatp  30993  cnvprop  31008  mptprop  31010  coprprop  31011  padct  31033  resf1o  31044  symgcom  31331  tocycfv  31355  tocycf  31363  tocyc01  31364  cycpm2tr  31365  cycpmco2f1  31370  cycpmco2rn  31371  cycpmconjv  31388  cycpmconjslem2  31401  idlsrgval  31627  rprmval  31643  zarclsun  31799  ordtprsval  31847  ordtprsuni  31848  ordtcnvNEW  31849  unelcarsg  32258  carsgclctunlem1  32263  eulerpartlemt  32317  sseqval  32334  probun  32365  bnj1373  32989  bnj1489  33015  cvmliftlem10  33235  satfvsuc  33302  satfdm  33310  satf0suc  33317  sat1el2xp  33320  fmlasuc0  33325  satffunlem1lem1  33343  satffunlem2lem1  33345  mrexval  33442  mrsubffval  33448  msrval  33479  mthmpps  33523  xpord2pred  33771  xpord3pred  33777  nodenselem5  33870  nosupbnd2lem1  33897  nosupbnd2  33898  noinfbnd2lem1  33912  noinfbnd2  33913  noetainflem2  33920  madeoldsuc  34046  lrold  34056  lrrecval  34075  addsval  34105  addsid1  34106  addscom  34108  addscllem1  34110  lineunray  34428  rdgssun  35528  exrecfnlem  35529  finixpnum  35741  ptrest  35755  poimirlem1  35757  poimirlem2  35758  poimirlem3  35759  poimirlem4  35760  poimirlem5  35761  poimirlem6  35762  poimirlem7  35763  poimirlem8  35764  poimirlem9  35765  poimirlem10  35766  poimirlem11  35767  poimirlem12  35768  poimirlem15  35771  poimirlem16  35772  poimirlem17  35773  poimirlem18  35774  poimirlem19  35775  poimirlem20  35776  poimirlem21  35777  poimirlem22  35778  poimirlem23  35779  poimirlem24  35780  poimirlem26  35782  poimirlem27  35783  poimirlem28  35784  poimirlem32  35788  mblfinlem2  35794  itg2addnclem2  35808  ldualset  37118  paddval  37791  paddcom  37806  dvafset  38997  dvaset  38998  dvhfset  39073  dvhset  39074  hdmapfval  39820  hlhilset  39927  metakunt17  40121  metakunt20  40124  metakunt21  40125  metakunt22  40126  metakunt24  40128  fsuppssindlem2  40261  istopclsd  40502  fzsplit1nn0  40556  diophrw  40561  eldioph2lem1  40562  eldioph2lem2  40563  diophin  40574  diophren  40615  pwssplit4  40894  mendval  40988  iocunico  41022  rclexi  41176  rtrclex  41178  rtrclexi  41182  cnvrcl0  41186  dfrtrcl5  41190  dfrcl2  41235  dfrcl3  41236  iunrelexp0  41263  trclfvdecomr  41289  dfrtrcl4  41299  frege131d  41325  clsk3nimkb  41603  clsk1indlem3  41606  clsk1independent  41609  ntrclskb  41632  ntrclsk3  41633  ntrclsk13  41634  dvmptfprodlem  43439  caratheodorylem1  44018  ovnsubadd2lem  44137  ovolval4lem1  44141  fzopredsuc  44767  mndpsuppss  45659  aacllem  46457