Theorem uneq12d 4122

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3903

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910

This theorem is referenced by:  symdifeq1  4208  csbun  4394  csbprg  4663  disjpr2  4667  diftpsn3  4756  iunxprg  5048  relresdm1  5988  rnpropg  6175  suceqd  6378  fntpg  6546  foun  6786  f1oprswap  6812  fnimapr  6910  fnimatpd  6911  xpprsng  7078  residpr  7081  fvsnun2  7123  fsnunfv  7127  fsnunres  7128  f1ounsn  7213  f1ofvswap  7247  xpord2pred  8085  xpord3pred  8092  frrlem12  8237  oarec  8487  ereq1  8639  mapunen  9070  cnfcomlem  9614  trcl  9643  djueq12  9819  r0weon  9925  infxpen  9927  cfsmolem  10183  cfsmo  10184  axdc3lem4  10366  ttukeylem3  10424  ttukey2g  10429  alephadd  10490  fpwwe2lem12  10555  wunex2  10651  wuncval2  10660  inar1  10688  prunioo  13402  fztp  13501  fzsuc2  13503  fseq1p1m1  13519  s3tpop  14834  s4dom  14844  s2rn  14888  s3rn  14889  s7rn  14890  trclun  14939  relexp0g  14947  relexpsucnnr  14950  dfrtrcl2  14987  setsvalg  17095  setsdm  17099  setsfun0  17101  setsid  17136  prdsval  17377  imasval  17433  mreexd  17566  mreexexlemd  17568  estrreslem2  18062  ipoval  18454  istsr  18507  mndpsuppss  18657  gsumzaddlem  19818  pwssplit1  20981  psrval  21840  psdmullem  22068  ordtval  23092  ordtcnv  23104  paste  23197  connsuba  23323  ptval2  23504  dfac14  23521  xkoptsub  23557  ptuncnv  23710  ptunhmeo  23711  xpstopnlem1  23712  alexsubALTlem3  23952  ustuqtop1  24145  rrxmvallem  25320  ovolioo  25485  uniiccdif  25495  itgsplitioo  25755  limcfval  25789  lhop2  25936  lgsquadlem2  27308  nodenselem5  27616  nosupbnd2lem1  27643  nosupbnd2  27644  noinfbnd2lem1  27658  noinfbnd2  27659  noetainflem2  27666  madeoldsuc  27817  lrold  27829  lrrecval  27869  addsval  27892  addsrid  27894  addscom  27896  addsproplem1  27899  addsprop  27906  addsass  27935  mulsval  28035  mulsrid  28039  mulsproplemcbv  28041  mulsproplem1  28042  mulsprop  28056  mulscom  28065  addsdi  28081  mulsass  28092  mulsunif2lem  28095  precsexlemcbv  28131  precsexlem3  28134  n0scut  28249  halfcut  28364  readdscl  28386  remulscl  28389  axlowdimlem13  28917  axlowdimlem15  28919  axlowdim  28924  eengv  28942  vtxdun  29445  trlsegvdeg  30189  numclwwlk3lem2lem  30345  ex-res  30403  imadifxp  32563  suppun2  32640  cnvprop  32652  mptprop  32654  coprprop  32655  fmptunsnop  32656  padct  32676  resf1o  32686  symgcom  33038  tocycfv  33064  tocycf  33072  tocyc01  33073  cycpm2tr  33074  cycpmco2f1  33079  cycpmco2rn  33080  cycpmconjv  33097  cycpmconjslem2  33110  elrgspnlem4  33198  rlocval  33212  idlsrgval  33453  rprmval  33466  zarclsun  33839  ordtprsval  33887  ordtprsuni  33888  ordtcnvNEW  33889  unelcarsg  34282  carsgclctunlem1  34287  eulerpartlemt  34341  sseqval  34358  probun  34389  bnj1373  34999  bnj1489  35025  cvmliftlem10  35269  satfvsuc  35336  satfdm  35344  satf0suc  35351  sat1el2xp  35354  fmlasuc0  35359  satffunlem1lem1  35377  satffunlem2lem1  35379  mrexval  35476  mrsubffval  35482  msrval  35513  mthmpps  35557  lineunray  36123  rdgssun  37354  exrecfnlem  37355  finixpnum  37587  ptrest  37601  poimirlem1  37603  poimirlem2  37604  poimirlem3  37605  poimirlem4  37606  poimirlem5  37607  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem9  37611  poimirlem10  37612  poimirlem11  37613  poimirlem12  37614  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem18  37620  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem23  37625  poimirlem24  37626  poimirlem26  37628  poimirlem27  37629  poimirlem28  37630  poimirlem32  37634  mblfinlem2  37640  itg2addnclem2  37654  ldualset  39106  paddval  39780  paddcom  39795  dvafset  40986  dvaset  40987  dvhfset  41062  dvhset  41063  hdmapfval  41809  hlhilset  41916  dvun  42335  fsuppssindlem2  42568  istopclsd  42676  fzsplit1nn0  42730  diophrw  42735  eldioph2lem1  42736  eldioph2lem2  42737  diophin  42748  diophren  42789  pwssplit4  43065  mendval  43155  iocunico  43187  tfsconcatun  43313  tfsconcat0i  43321  onsucunitp  43349  oaun3  43358  rclexi  43591  rtrclex  43593  rtrclexi  43597  cnvrcl0  43601  dfrtrcl5  43605  dfrcl2  43650  dfrcl3  43651  iunrelexp0  43678  trclfvdecomr  43704  dfrtrcl4  43714  frege131d  43740  clsk3nimkb  44016  clsk1indlem3  44019  clsk1independent  44022  ntrclskb  44045  ntrclsk3  44046  ntrclsk13  44047  permaxinf2lem  44989  dvmptfprodlem  45929  caratheodorylem1  46511  ovnsubadd2lem  46630  ovolval4lem1  46634  fzopredsuc  47311  clnbgrval  47810  cycl3grtri  47935  aacllem  49790