Theorem uneq12d 4025

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

Syntax hints:   → wi 4   = wceq 1507   ∪ cun 3823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-un 3830

This theorem is referenced by:  symdifeq1  4103  csbun  4268  csbprg  4513  disjpr2  4517  diftpsn3  4603  iunxprg  4878  rnpropg  5912  suceq  6088  fntpg  6241  foun  6456  f1oprswap  6481  fnimapr  6569  xpprsng  6719  residpr  6722  fvsnun2  6764  fsnunfv  6770  fsnunres  6771  oarec  7981  ereq1  8088  mapunen  8474  cnfcomlem  8948  trcl  8956  djueq12  9119  r0weon  9224  infxpen  9226  cfsmolem  9482  cfsmo  9483  axdc3lem4  9665  ttukeylem3  9723  ttukey2g  9728  alephadd  9789  fpwwe2lem13  9854  wunex2  9950  wuncval2  9959  inar1  9987  prunioo  12676  fztp  12772  fzsuc2  12774  fseq1p1m1  12790  s3tpop  14123  s4dom  14133  trclun  14225  relexp0g  14232  relexpsucnnr  14235  dfrtrcl2  14272  setsvalg  16358  setsdm  16363  setsfun0  16365  setsid  16384  prdsval  16574  imasval  16630  mreexd  16761  mreexexlemd  16763  estrreslem2  17236  ipoval  17612  istsr  17675  gsumzaddlem  18784  pwssplit1  19543  psrval  19846  ordtval  21491  ordtcnv  21503  paste  21596  connsuba  21722  ptval2  21903  dfac14  21920  xkoptsub  21956  ptuncnv  22109  ptunhmeo  22110  xpstopnlem1  22111  alexsubALTlem3  22351  ustuqtop1  22543  rrxmvallem  23700  ovolioo  23862  uniiccdif  23872  itgsplitioo  24131  limcfval  24163  lhop2  24305  lgsquadlem2  25649  axlowdimlem13  26433  axlowdimlem15  26435  axlowdim  26440  eengv  26458  vtxdun  26956  trlsegvdeg  27747  numclwwlk3lem2lem  27930  ex-res  27988  imadifxp  30107  funresdm1  30109  padct  30196  resf1o  30207  ordtprsval  30762  ordtprsuni  30763  ordtcnvNEW  30764  unelcarsg  31172  carsgclctunlem1  31177  eulerpartlemt  31231  sseqval  31249  probun  31280  bnj1373  31908  bnj1489  31934  cvmliftlem10  32086  mrexval  32208  mrsubffval  32214  msrval  32245  mthmpps  32289  frrlem12  32595  nodenselem5  32653  nosupbnd2lem1  32676  nosupbnd2  32677  lineunray  33069  rdgssun  34036  exrecfnlem  34037  finixpnum  34266  ptrest  34280  poimirlem1  34282  poimirlem2  34283  poimirlem3  34284  poimirlem4  34285  poimirlem5  34286  poimirlem6  34287  poimirlem7  34288  poimirlem8  34289  poimirlem9  34290  poimirlem10  34291  poimirlem11  34292  poimirlem12  34293  poimirlem15  34296  poimirlem16  34297  poimirlem17  34298  poimirlem18  34299  poimirlem19  34300  poimirlem20  34301  poimirlem21  34302  poimirlem22  34303  poimirlem23  34304  poimirlem24  34305  poimirlem26  34307  poimirlem27  34308  poimirlem28  34309  poimirlem32  34313  mblfinlem2  34319  itg2addnclem2  34333  ldualset  35654  paddval  36327  paddcom  36342  dvafset  37533  dvaset  37534  dvhfset  37609  dvhset  37610  hdmapfval  38356  hlhilset  38463  istopclsd  38637  fzsplit1nn0  38691  diophrw  38696  eldioph2lem1  38697  eldioph2lem2  38698  diophin  38710  diophren  38751  pwssplit4  39030  mendval  39124  iocunico  39158  rclexi  39283  rtrclex  39285  rtrclexi  39289  cnvrcl0  39293  dfrtrcl5  39297  dfrcl2  39327  dfrcl3  39328  iunrelexp0  39355  trclfvdecomr  39381  dfrtrcl4  39391  frege131d  39417  clsk3nimkb  39698  clsk1indlem3  39701  clsk1independent  39704  ntrclskb  39727  ntrclsk3  39728  ntrclsk13  39729  dvmptfprodlem  41605  caratheodorylem1  42185  ovnsubadd2lem  42304  ovolval4lem1  42308  fzopredsuc  42875  mndpsuppss  43725  aacllem  44209