Theorem uneq12d 4163

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

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3945

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952

This theorem is referenced by:  symdifeq1  4243  csbun  4437  csbprg  4712  disjpr2  4716  diftpsn3  4804  iunxprg  5098  relresdm1  6032  rnpropg  6220  suceq  6429  fntpg  6607  foun  6850  f1oprswap  6876  fnimapr  6974  xpprsng  7139  residpr  7142  fvsnun2  7182  fsnunfv  7186  fsnunres  7187  f1ofvswap  7306  xpord2pred  8133  xpord3pred  8140  frrlem12  8284  oarec  8564  ereq1  8712  mapunen  9148  cnfcomlem  9696  trcl  9725  djueq12  9901  r0weon  10009  infxpen  10011  cfsmolem  10267  cfsmo  10268  axdc3lem4  10450  ttukeylem3  10508  ttukey2g  10513  alephadd  10574  fpwwe2lem12  10639  wunex2  10735  wuncval2  10744  inar1  10772  prunioo  13462  fztp  13561  fzsuc2  13563  fseq1p1m1  13579  s3tpop  14864  s4dom  14874  trclun  14965  relexp0g  14973  relexpsucnnr  14976  dfrtrcl2  15013  setsvalg  17103  setsdm  17107  setsfun0  17109  setsid  17145  prdsval  17405  imasval  17461  mreexd  17590  mreexexlemd  17592  estrreslem2  18094  ipoval  18487  istsr  18540  gsumzaddlem  19830  pwssplit1  20814  psrval  21687  ordtval  22913  ordtcnv  22925  paste  23018  connsuba  23144  ptval2  23325  dfac14  23342  xkoptsub  23378  ptuncnv  23531  ptunhmeo  23532  xpstopnlem1  23533  alexsubALTlem3  23773  ustuqtop1  23966  rrxmvallem  25152  ovolioo  25317  uniiccdif  25327  itgsplitioo  25587  limcfval  25621  lhop2  25767  lgsquadlem2  27120  nodenselem5  27427  nosupbnd2lem1  27454  nosupbnd2  27455  noinfbnd2lem1  27469  noinfbnd2  27470  noetainflem2  27477  madeoldsuc  27616  lrold  27628  lrrecval  27661  addsval  27684  addsrid  27686  addscom  27688  addsproplem1  27691  addsprop  27698  addsass  27727  mulsval  27804  mulsrid  27808  mulsproplemcbv  27810  mulsproplem1  27811  mulsprop  27825  mulscom  27834  addsdi  27849  mulsass  27860  precsexlemcbv  27891  precsexlem3  27894  n0scut  27943  axlowdimlem13  28479  axlowdimlem15  28481  axlowdim  28486  eengv  28504  vtxdun  29005  trlsegvdeg  29747  numclwwlk3lem2lem  29903  ex-res  29961  imadifxp  32099  fnimatp  32169  cnvprop  32185  mptprop  32187  coprprop  32188  padct  32211  resf1o  32222  symgcom  32514  tocycfv  32538  tocycf  32546  tocyc01  32547  cycpm2tr  32548  cycpmco2f1  32553  cycpmco2rn  32554  cycpmconjv  32571  cycpmconjslem2  32584  idlsrgval  32891  rprmval  32907  zarclsun  33148  ordtprsval  33196  ordtprsuni  33197  ordtcnvNEW  33198  unelcarsg  33609  carsgclctunlem1  33614  eulerpartlemt  33668  sseqval  33685  probun  33716  bnj1373  34339  bnj1489  34365  cvmliftlem10  34583  satfvsuc  34650  satfdm  34658  satf0suc  34665  sat1el2xp  34668  fmlasuc0  34673  satffunlem1lem1  34691  satffunlem2lem1  34693  mrexval  34790  mrsubffval  34796  msrval  34827  mthmpps  34871  lineunray  35423  rdgssun  36562  exrecfnlem  36563  finixpnum  36776  ptrest  36790  poimirlem1  36792  poimirlem2  36793  poimirlem3  36794  poimirlem4  36795  poimirlem5  36796  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem9  36800  poimirlem10  36801  poimirlem11  36802  poimirlem12  36803  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem18  36809  poimirlem19  36810  poimirlem20  36811  poimirlem21  36812  poimirlem22  36813  poimirlem23  36814  poimirlem24  36815  poimirlem26  36817  poimirlem27  36818  poimirlem28  36819  poimirlem32  36823  mblfinlem2  36829  itg2addnclem2  36843  ldualset  38298  paddval  38972  paddcom  38987  dvafset  40178  dvaset  40179  dvhfset  40254  dvhset  40255  hdmapfval  41001  hlhilset  41108  metakunt17  41307  metakunt20  41310  metakunt21  41311  metakunt22  41312  metakunt24  41314  fsuppssindlem2  41466  istopclsd  41740  fzsplit1nn0  41794  diophrw  41799  eldioph2lem1  41800  eldioph2lem2  41801  diophin  41812  diophren  41853  pwssplit4  42133  mendval  42227  iocunico  42262  tfsconcatun  42389  tfsconcat0i  42397  onsucunitp  42425  oaun3  42434  rclexi  42668  rtrclex  42670  rtrclexi  42674  cnvrcl0  42678  dfrtrcl5  42682  dfrcl2  42727  dfrcl3  42728  iunrelexp0  42755  trclfvdecomr  42781  dfrtrcl4  42791  frege131d  42817  clsk3nimkb  43093  clsk1indlem3  43096  clsk1independent  43099  ntrclskb  43122  ntrclsk3  43123  ntrclsk13  43124  dvmptfprodlem  44958  caratheodorylem1  45540  ovnsubadd2lem  45659  ovolval4lem1  45663  fzopredsuc  46329  mndpsuppss  47135  aacllem  47935