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  4666  disjpr2  4670  diftpsn3  4761  iunxprg  5055  relresdm1  6024  rnpropg  6223  suceqd  6430  fntpg  6601  foun  6844  f1oprswap  6871  fnimapr  6969  fnimatpd  6970  xpprsng  7143  xpsnprg  7144  xpsntpg  7145  residpr  7147  fvsnun2  7189  fsnunfv  7193  fsnunres  7194  f1ounsn  7281  f1ofvswap  7315  xpord2pred  8165  xpord3pred  8172  frrlem12  8319  oarec  8574  ereq1  8729  mapunen  9169  cnfcomlem  9704  trcl  9733  djueq12  9989  r0weon  10095  infxpen  10097  cfsmolem  10352  cfsmo  10353  axdc3lem4  10535  ttukeylem3  10593  ttukey2g  10598  alephadd  10666  fpwwe2lem12  10731  wunex2  10827  wuncval2  10836  inar1  10864  prunioo  13616  fztp  13718  fzsuc2  13720  fseq1p1m1  13736  s3tpop  15066  s4dom  15076  s2rn  15122  s3rn  15123  s7rn  15124  trclun  15173  relexp0g  15181  relexpsucnnr  15184  dfrtrcl2  15221  setsvalg  17350  setsdm  17354  setsfun0  17356  setsid  17391  prdsval  17632  imasval  17689  mreexd  17822  mreexexlemd  17824  estrreslem2  18318  ipoval  18710  istsr  18763  mndpsuppss  18965  gsumzaddlem  20141  pwssplit1  21340  psrval  22229  psdmullem  22492  ordtval  23513  ordtcnv  23525  paste  23618  connsuba  23744  ptval2  23926  dfac14  23943  xkoptsub  23979  ptuncnv  24132  ptunhmeo  24133  xpstopnlem1  24134  alexsubALTlem3  24374  ustuqtop1  24566  rrxmvallem  25731  ovolioo  25895  uniiccdif  25905  itgsplitioo  26164  limcfval  26198  lhop2  26341  lgsquadlem2  27714  nodenselem5  28051  nosupbnd2lem1  28078  nosupbnd2  28079  noinfbnd2lem1  28093  noinfbnd2  28094  noetainflem2  28101  madeoldsuc  28277  lrold  28289  lrrecval  28331  addsval  28354  addsrid  28356  addscom  28358  addsproplem1  28361  addsprop  28368  addsass  28397  mulsval  28501  mulsrid  28505  mulsproplemcbv  28507  mulsproplem1  28508  mulsprop  28522  mulscom  28531  addsdi  28547  mulsass  28558  mulsunif2lem  28561  precsexlemcbv  28598  precsexlem3  28601  n0cut  28726  halfcut  28850  pw2cut2  28854  readdscl  28891  remulscl  28894  axlowdimlem13  29538  axlowdimlem15  29540  axlowdim  29545  eengv  29563  vtxdun  30068  trlsegvdeg  30834  numclwwlk3lem2lem  30990  ex-res  31048  imadifxp  33243  fresunsn  33267  suppun2  33325  cnvprop  33337  mptprop  33339  coprprop  33340  fmptunsnop  33341  padct  33358  resf1o  33369  symgcom  33691  tocycfv  33717  tocycf  33725  tocyc01  33726  cycpm2tr  33727  cycpmco2f1  33732  cycpmco2rn  33733  cycpmconjv  33750  cycpmconjslem2  33763  elrgspnlem4  33853  rlocval  33867  idlsrgval  34082  rprmval  34095  extvfvcl  34215  zarclsun  34549  ordtprsval  34597  ordtprsuni  34598  ordtcnvNEW  34599  unelcarsg  34991  carsgclctunlem1  34996  eulerpartlemt  35050  sseqval  35067  probun  35098  bnj1373  35707  bnj1489  35733  brr0d  35941  cvmliftlem10  36146  satfvsuc  36213  satfdm  36221  satf0suc  36228  sat1el2xp  36231  fmlasuc0  36236  satffunlem1lem1  36254  satffunlem2lem1  36256  mrexval  36353  mrsubffval  36359  msrval  36390  mthmpps  36434  lineunray  37005  rdgssun  38395  exrecfnlem  38396  finixpnum  38622  ptrest  38631  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem4  38636  poimirlem5  38637  poimirlem6  38638  poimirlem7  38639  poimirlem8  38640  poimirlem9  38641  poimirlem10  38642  poimirlem11  38643  poimirlem12  38644  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem18  38650  poimirlem19  38651  poimirlem20  38652  poimirlem21  38653  poimirlem22  38654  poimirlem23  38655  poimirlem24  38656  poimirlem26  38658  poimirlem27  38659  poimirlem28  38660  poimirlem32  38664  mblfinlem2  38670  itg2addnclem2  38684  ecun  39419  ecuncnvepres  39421  ldualset  40276  paddval  40949  paddcom  40964  dvafset  42155  dvaset  42156  dvhfset  42231  dvhset  42232  hdmapfval  42978  hlhilset  43085  dvun  43504  fsuppssindlem2  43714  istopclsd  43805  fzsplit1nn0  43859  diophrw  43864  eldioph2lem1  43865  eldioph2lem2  43866  diophin  43877  diophren  43914  pwssplit4  44185  mendval  44275  iocunico  44307  tfsconcatun  44433  tfsconcat0i  44441  onsucunitp  44469  oaun3  44478  rclexi  44709  rtrclex  44711  rtrclexi  44715  cnvrcl0  44719  dfrtrcl5  44723  dfrcl2  44768  dfrcl3  44769  iunrelexp0  44796  trclfvdecomr  44822  dfrtrcl4  44832  frege131d  44858  clsk3nimkb  45134  clsk1indlem3  45137  clsk1independent  45140  ntrclskb  45163  ntrclsk3  45164  ntrclsk13  45165  permaxinf2lem  46096  dvmptfprodlem  47048  caratheodorylem1  47630  ovnsubadd2lem  47749  ovolval4lem1  47753  fzopredsuc  48488  clnbgrval  49014  cycl3grtri  49139  aacllem  51108