Theorem uneq12d 4168

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151

This theorem is used by:  symdifeq1  4200  csbun  4398  csbprg  4669  disjpr2  4673  diftpsn3  4764  iunxprg  5055  relresdm1  6024  rnpropg  6223  suceqd  6430  fntpg  6600  foun  6843  f1oprswap  6870  fnimapr  6968  fnimatpd  6969  xpprsng  7142  xpsnprg  7143  xpsntpg  7144  residpr  7146  fvsnun2  7188  fsnunfv  7192  fsnunres  7193  f1ounsn  7280  f1ofvswap  7314  xpord2pred  8162  xpord3pred  8169  frrlem12  8316  oarec  8571  ereq1  8726  mapunen  9166  cnfcomlem  9701  trcl  9730  djueq12  9986  r0weon  10092  infxpen  10094  cfsmolem  10349  cfsmo  10350  axdc3lem4  10532  ttukeylem3  10590  ttukey2g  10595  alephadd  10663  fpwwe2lem12  10728  wunex2  10824  wuncval2  10833  inar1  10861  prunioo  13613  fztp  13715  fzsuc2  13717  fseq1p1m1  13733  s3tpop  15061  s4dom  15071  s2rn  15117  s3rn  15118  s7rn  15119  trclun  15168  relexp0g  15176  relexpsucnnr  15179  dfrtrcl2  15216  setsvalg  17345  setsdm  17349  setsfun0  17351  setsid  17386  prdsval  17627  imasval  17684  mreexd  17817  mreexexlemd  17819  estrreslem2  18313  ipoval  18705  istsr  18758  mndpsuppss  18960  gsumzaddlem  20136  pwssplit1  21335  psrval  22224  psdmullem  22487  ordtval  23508  ordtcnv  23520  paste  23613  connsuba  23739  ptval2  23921  dfac14  23938  xkoptsub  23974  ptuncnv  24127  ptunhmeo  24128  xpstopnlem1  24129  alexsubALTlem3  24369  ustuqtop1  24561  rrxmvallem  25726  ovolioo  25890  uniiccdif  25900  itgsplitioo  26159  limcfval  26193  lhop2  26336  lgsquadlem2  27709  nodenselem5  28046  nosupbnd2lem1  28073  nosupbnd2  28074  noinfbnd2lem1  28088  noinfbnd2  28089  noetainflem2  28096  madeoldsuc  28272  lrold  28284  lrrecval  28326  addsval  28349  addsrid  28351  addscom  28353  addsproplem1  28356  addsprop  28363  addsass  28392  mulsval  28496  mulsrid  28500  mulsproplemcbv  28502  mulsproplem1  28503  mulsprop  28517  mulscom  28526  addsdi  28542  mulsass  28553  mulsunif2lem  28556  precsexlemcbv  28593  precsexlem3  28596  n0cut  28721  halfcut  28845  pw2cut2  28849  readdscl  28886  remulscl  28889  axlowdimlem13  29533  axlowdimlem15  29535  axlowdim  29540  eengv  29558  vtxdun  30063  trlsegvdeg  30829  numclwwlk3lem2lem  30985  ex-res  31043  imadifxp  33238  fresunsn  33262  suppun2  33320  cnvprop  33332  mptprop  33334  coprprop  33335  fmptunsnop  33336  padct  33353  resf1o  33365  symgcom  33687  tocycfv  33713  tocycf  33721  tocyc01  33722  cycpm2tr  33723  cycpmco2f1  33728  cycpmco2rn  33729  cycpmconjv  33746  cycpmconjslem2  33759  elrgspnlem4  33849  rlocval  33863  idlsrgval  34078  rprmval  34091  extvfvcl  34211  zarclsun  34545  ordtprsval  34593  ordtprsuni  34594  ordtcnvNEW  34595  unelcarsg  34987  carsgclctunlem1  34992  eulerpartlemt  35046  sseqval  35063  probun  35094  bnj1373  35703  bnj1489  35729  cvmliftlem10  36102  satfvsuc  36169  satfdm  36177  satf0suc  36184  sat1el2xp  36187  fmlasuc0  36192  satffunlem1lem1  36210  satffunlem2lem1  36212  mrexval  36309  mrsubffval  36315  msrval  36346  mthmpps  36390  lineunray  36955  rdgssun  38345  exrecfnlem  38346  finixpnum  38572  ptrest  38581  poimirlem1  38583  poimirlem2  38584  poimirlem3  38585  poimirlem4  38586  poimirlem5  38587  poimirlem6  38588  poimirlem7  38589  poimirlem8  38590  poimirlem9  38591  poimirlem10  38592  poimirlem11  38593  poimirlem12  38594  poimirlem15  38597  poimirlem16  38598  poimirlem17  38599  poimirlem18  38600  poimirlem19  38601  poimirlem20  38602  poimirlem21  38603  poimirlem22  38604  poimirlem23  38605  poimirlem24  38606  poimirlem26  38608  poimirlem27  38609  poimirlem28  38610  poimirlem32  38614  mblfinlem2  38620  itg2addnclem2  38634  ecun  39369  ecuncnvepres  39371  ldualset  40226  paddval  40899  paddcom  40914  dvafset  42105  dvaset  42106  dvhfset  42181  dvhset  42182  hdmapfval  42928  hlhilset  43035  dvun  43454  fsuppssindlem2  43664  istopclsd  43755  fzsplit1nn0  43809  diophrw  43814  eldioph2lem1  43815  eldioph2lem2  43816  diophin  43827  diophren  43864  pwssplit4  44135  mendval  44225  iocunico  44257  tfsconcatun  44383  tfsconcat0i  44391  onsucunitp  44419  oaun3  44428  rclexi  44659  rtrclex  44661  rtrclexi  44665  cnvrcl0  44669  dfrtrcl5  44673  dfrcl2  44718  dfrcl3  44719  iunrelexp0  44746  trclfvdecomr  44772  dfrtrcl4  44782  frege131d  44808  clsk3nimkb  45084  clsk1indlem3  45087  clsk1independent  45090  ntrclskb  45113  ntrclsk3  45114  ntrclsk13  45115  permaxinf2lem  46046  dvmptfprodlem  46998  caratheodorylem1  47580  ovnsubadd2lem  47699  ovolval4lem1  47703  fzopredsuc  48438  clnbgrval  48964  cycl3grtri  49089  aacllem  50983