Theorem uneq12d 4106

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

Syntax hints:   → wi 4   = wceq 1547   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895

This theorem is referenced by:  symdifeq1  4190  csbun  4376  csbprg  4648  disjpr2  4652  diftpsn3  4742  iunxprg  5032  relresdm1  5992  rnpropg  6180  suceqd  6384  fntpg  6552  foun  6792  f1oprswap  6819  fnimapr  6917  fnimatpd  6918  xpprsng  7089  residpr  7092  fvsnun2  7134  fsnunfv  7138  fsnunres  7139  f1ounsn  7223  f1ofvswap  7257  xpord2pred  8092  xpord3pred  8099  frrlem12  8244  oarec  8494  ereq1  8648  mapunen  9081  cnfcomlem  9618  trcl  9647  djueq12  9826  r0weon  9932  infxpen  9934  cfsmolem  10190  cfsmo  10191  axdc3lem4  10373  ttukeylem3  10431  ttukey2g  10436  alephadd  10498  fpwwe2lem12  10563  wunex2  10659  wuncval2  10668  inar1  10696  prunioo  13432  fztp  13532  fzsuc2  13534  fseq1p1m1  13550  s3tpop  14869  s4dom  14879  s2rn  14923  s3rn  14924  s7rn  14925  trclun  14974  relexp0g  14982  relexpsucnnr  14985  dfrtrcl2  15022  setsvalg  17134  setsdm  17138  setsfun0  17140  setsid  17175  prdsval  17416  imasval  17473  mreexd  17606  mreexexlemd  17608  estrreslem2  18102  ipoval  18494  istsr  18547  mndpsuppss  18731  gsumzaddlem  19894  pwssplit1  21056  psrval  21897  psdmullem  22160  ordtval  23179  ordtcnv  23191  paste  23284  connsuba  23410  ptval2  23591  dfac14  23608  xkoptsub  23644  ptuncnv  23797  ptunhmeo  23798  xpstopnlem1  23799  alexsubALTlem3  24039  ustuqtop1  24231  rrxmvallem  25396  ovolioo  25560  uniiccdif  25570  itgsplitioo  25830  limcfval  25864  lhop2  26007  lgsquadlem2  27369  nodenselem5  27677  nosupbnd2lem1  27704  nosupbnd2  27705  noinfbnd2lem1  27719  noinfbnd2  27720  noetainflem2  27727  madeoldsuc  27902  lrold  27914  lrrecval  27956  addsval  27979  addsrid  27981  addscom  27983  addsproplem1  27986  addsprop  27993  addsass  28022  mulsval  28126  mulsrid  28130  mulsproplemcbv  28132  mulsproplem1  28133  mulsprop  28147  mulscom  28156  addsdi  28172  mulsass  28183  mulsunif2lem  28186  precsexlemcbv  28223  precsexlem3  28226  n0cut  28351  halfcut  28475  pw2cut2  28479  readdscl  28516  remulscl  28519  axlowdimlem13  29048  axlowdimlem15  29050  axlowdim  29055  eengv  29073  vtxdun  29575  trlsegvdeg  30322  numclwwlk3lem2lem  30478  ex-res  30536  imadifxp  32697  fresunsn  32724  suppun2  32783  cnvprop  32795  mptprop  32797  coprprop  32798  fmptunsnop  32799  padct  32817  resf1o  32829  symgcom  33171  tocycfv  33197  tocycf  33205  tocyc01  33206  cycpm2tr  33207  cycpmco2f1  33212  cycpmco2rn  33213  cycpmconjv  33230  cycpmconjslem2  33243  elrgspnlem4  33333  rlocval  33347  idlsrgval  33593  rprmval  33606  extvfvcl  33727  zarclsun  34061  ordtprsval  34109  ordtprsuni  34110  ordtcnvNEW  34111  unelcarsg  34503  carsgclctunlem1  34508  eulerpartlemt  34562  sseqval  34579  probun  34610  bnj1373  35219  bnj1489  35245  cvmliftlem10  35529  satfvsuc  35596  satfdm  35604  satf0suc  35611  sat1el2xp  35614  fmlasuc0  35619  satffunlem1lem1  35637  satffunlem2lem1  35639  mrexval  35736  mrsubffval  35742  msrval  35773  mthmpps  35817  lineunray  36382  rdgssun  37747  exrecfnlem  37748  finixpnum  37979  ptrest  37993  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem9  38003  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem18  38012  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem23  38017  poimirlem24  38018  poimirlem26  38020  poimirlem27  38021  poimirlem28  38022  poimirlem32  38026  mblfinlem2  38032  itg2addnclem2  38046  ecun  38767  ecuncnvepres  38769  ldualset  39624  paddval  40297  paddcom  40312  dvafset  41503  dvaset  41504  dvhfset  41579  dvhset  41580  hdmapfval  42326  hlhilset  42433  dvun  42843  fsuppssindlem2  43049  istopclsd  43156  fzsplit1nn0  43210  diophrw  43215  eldioph2lem1  43216  eldioph2lem2  43217  diophin  43228  diophren  43265  pwssplit4  43541  mendval  43631  iocunico  43663  tfsconcatun  43789  tfsconcat0i  43797  onsucunitp  43825  oaun3  43834  rclexi  44066  rtrclex  44068  rtrclexi  44072  cnvrcl0  44076  dfrtrcl5  44080  dfrcl2  44125  dfrcl3  44126  iunrelexp0  44153  trclfvdecomr  44179  dfrtrcl4  44189  frege131d  44215  clsk3nimkb  44491  clsk1indlem3  44494  clsk1independent  44497  ntrclskb  44520  ntrclsk3  44521  ntrclsk13  44522  permaxinf2lem  45463  dvmptfprodlem  46394  caratheodorylem1  46976  ovnsubadd2lem  47095  ovolval4lem1  47099  fzopredsuc  47794  clnbgrval  48320  cycl3grtri  48445  aacllem  50298