Theorem uneq12d 4192

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

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  symdifeq1  4274  csbun  4464  csbprg  4734  disjpr2  4738  diftpsn3  4827  iunxprg  5119  relresdm1  6062  rnpropg  6253  suceq  6461  fntpg  6638  foun  6880  f1oprswap  6906  fnimapr  7005  fnimatpd  7006  xpprsng  7174  residpr  7177  fvsnun2  7217  fsnunfv  7221  fsnunres  7222  f1ofvswap  7342  xpord2pred  8186  xpord3pred  8193  frrlem12  8338  oarec  8618  ereq1  8770  mapunen  9212  cnfcomlem  9768  trcl  9797  djueq12  9973  r0weon  10081  infxpen  10083  cfsmolem  10339  cfsmo  10340  axdc3lem4  10522  ttukeylem3  10580  ttukey2g  10585  alephadd  10646  fpwwe2lem12  10711  wunex2  10807  wuncval2  10816  inar1  10844  prunioo  13541  fztp  13640  fzsuc2  13642  fseq1p1m1  13658  s3tpop  14958  s4dom  14968  s2rn  15012  s3rn  15013  s7rn  15014  trclun  15063  relexp0g  15071  relexpsucnnr  15074  dfrtrcl2  15111  setsvalg  17213  setsdm  17217  setsfun0  17219  setsid  17255  prdsval  17515  imasval  17571  mreexd  17700  mreexexlemd  17702  estrreslem2  18207  ipoval  18600  istsr  18653  gsumzaddlem  19963  pwssplit1  21081  psrval  21958  psdmullem  22192  ordtval  23218  ordtcnv  23230  paste  23323  connsuba  23449  ptval2  23630  dfac14  23647  xkoptsub  23683  ptuncnv  23836  ptunhmeo  23837  xpstopnlem1  23838  alexsubALTlem3  24078  ustuqtop1  24271  rrxmvallem  25457  ovolioo  25622  uniiccdif  25632  itgsplitioo  25893  limcfval  25927  lhop2  26074  lgsquadlem2  27443  nodenselem5  27751  nosupbnd2lem1  27778  nosupbnd2  27779  noinfbnd2lem1  27793  noinfbnd2  27794  noetainflem2  27801  madeoldsuc  27941  lrold  27953  lrrecval  27990  addsval  28013  addsrid  28015  addscom  28017  addsproplem1  28020  addsprop  28027  addsass  28056  mulsval  28153  mulsrid  28157  mulsproplemcbv  28159  mulsproplem1  28160  mulsprop  28174  mulscom  28183  addsdi  28199  mulsass  28210  mulsunif2lem  28213  precsexlemcbv  28248  precsexlem3  28251  n0scut  28356  halfcut  28434  pw2bday  28436  readdscl  28449  remulscl  28452  axlowdimlem13  28987  axlowdimlem15  28989  axlowdim  28994  eengv  29012  vtxdun  29517  trlsegvdeg  30259  numclwwlk3lem2lem  30415  ex-res  30473  imadifxp  32623  cnvprop  32708  mptprop  32710  coprprop  32711  padct  32733  resf1o  32744  symgcom  33076  tocycfv  33102  tocycf  33110  tocyc01  33111  cycpm2tr  33112  cycpmco2f1  33117  cycpmco2rn  33118  cycpmconjv  33135  cycpmconjslem2  33148  rlocval  33231  idlsrgval  33496  rprmval  33509  zarclsun  33816  ordtprsval  33864  ordtprsuni  33865  ordtcnvNEW  33866  unelcarsg  34277  carsgclctunlem1  34282  eulerpartlemt  34336  sseqval  34353  probun  34384  bnj1373  35006  bnj1489  35032  cvmliftlem10  35262  satfvsuc  35329  satfdm  35337  satf0suc  35344  sat1el2xp  35347  fmlasuc0  35352  satffunlem1lem1  35370  satffunlem2lem1  35372  mrexval  35469  mrsubffval  35475  msrval  35506  mthmpps  35550  lineunray  36111  rdgssun  37344  exrecfnlem  37345  finixpnum  37565  ptrest  37579  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem9  37589  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem32  37612  mblfinlem2  37618  itg2addnclem2  37632  ldualset  39081  paddval  39755  paddcom  39770  dvafset  40961  dvaset  40962  dvhfset  41037  dvhset  41038  hdmapfval  41784  hlhilset  41891  metakunt17  42178  metakunt20  42181  metakunt21  42182  metakunt22  42183  metakunt24  42185  fsuppssindlem2  42547  istopclsd  42656  fzsplit1nn0  42710  diophrw  42715  eldioph2lem1  42716  eldioph2lem2  42717  diophin  42728  diophren  42769  pwssplit4  43046  mendval  43140  iocunico  43172  tfsconcatun  43299  tfsconcat0i  43307  onsucunitp  43335  oaun3  43344  rclexi  43577  rtrclex  43579  rtrclexi  43583  cnvrcl0  43587  dfrtrcl5  43591  dfrcl2  43636  dfrcl3  43637  iunrelexp0  43664  trclfvdecomr  43690  dfrtrcl4  43700  frege131d  43726  clsk3nimkb  44002  clsk1indlem3  44005  clsk1independent  44008  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  dvmptfprodlem  45865  caratheodorylem1  46447  ovnsubadd2lem  46566  ovolval4lem1  46570  fzopredsuc  47238  clnbgrval  47696  mndpsuppss  48096  aacllem  48895