Theorem uneq12d 4126

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913

This theorem is used by:  symdifeq1  4211  csbun  4409  csbprg  4680  disjpr2  4684  diftpsn3  4775  iunxprg  5067  relresdm1  6040  rnpropg  6228  suceqd  6435  fntpg  6603  foun  6846  f1oprswap  6873  fnimapr  6971  fnimatpd  6972  xpprsng  7143  residpr  7146  fvsnun2  7188  fsnunfv  7192  fsnunres  7193  f1ounsn  7281  f1ofvswap  7315  xpord2pred  8150  xpord3pred  8157  frrlem12  8303  oarec  8556  ereq1  8711  mapunen  9144  cnfcomlem  9678  trcl  9707  djueq12  9909  r0weon  10015  infxpen  10017  cfsmolem  10272  cfsmo  10273  axdc3lem4  10455  ttukeylem3  10513  ttukey2g  10518  alephadd  10580  fpwwe2lem12  10645  wunex2  10741  wuncval2  10750  inar1  10778  prunioo  13526  fztp  13627  fzsuc2  13629  fseq1p1m1  13645  s3tpop  14972  s4dom  14982  s2rn  15026  s3rn  15027  s7rn  15028  trclun  15077  relexp0g  15085  relexpsucnnr  15088  dfrtrcl2  15125  setsvalg  17251  setsdm  17255  setsfun0  17257  setsid  17292  prdsval  17533  imasval  17590  mreexd  17723  mreexexlemd  17725  estrreslem2  18219  ipoval  18611  istsr  18664  mndpsuppss  18854  gsumzaddlem  20022  pwssplit1  21217  psrval  22102  psdmullem  22365  ordtval  23383  ordtcnv  23395  paste  23488  connsuba  23614  ptval2  23795  dfac14  23812  xkoptsub  23848  ptuncnv  24001  ptunhmeo  24002  xpstopnlem1  24003  alexsubALTlem3  24243  ustuqtop1  24435  rrxmvallem  25600  ovolioo  25764  uniiccdif  25774  itgsplitioo  26034  limcfval  26068  lhop2  26211  lgsquadlem2  27582  nodenselem5  27889  nosupbnd2lem1  27916  nosupbnd2  27917  noinfbnd2lem1  27931  noinfbnd2  27932  noetainflem2  27939  madeoldsuc  28115  lrold  28127  lrrecval  28169  addsval  28192  addsrid  28194  addscom  28196  addsproplem1  28199  addsprop  28206  addsass  28235  mulsval  28339  mulsrid  28343  mulsproplemcbv  28345  mulsproplem1  28346  mulsprop  28360  mulscom  28369  addsdi  28385  mulsass  28396  mulsunif2lem  28399  precsexlemcbv  28436  precsexlem3  28439  n0cut  28564  halfcut  28688  pw2cut2  28692  readdscl  28729  remulscl  28732  axlowdimlem13  29341  axlowdimlem15  29343  axlowdim  29348  eengv  29366  vtxdun  29868  trlsegvdeg  30615  numclwwlk3lem2lem  30771  ex-res  30829  imadifxp  32983  fresunsn  33007  suppun2  33066  cnvprop  33078  mptprop  33080  coprprop  33081  fmptunsnop  33082  padct  33100  resf1o  33112  symgcom  33434  tocycfv  33460  tocycf  33468  tocyc01  33469  cycpm2tr  33470  cycpmco2f1  33475  cycpmco2rn  33476  cycpmconjv  33493  cycpmconjslem2  33506  elrgspnlem4  33596  rlocval  33610  idlsrgval  33824  rprmval  33837  extvfvcl  33957  zarclsun  34291  ordtprsval  34339  ordtprsuni  34340  ordtcnvNEW  34341  unelcarsg  34734  carsgclctunlem1  34739  eulerpartlemt  34793  sseqval  34810  probun  34841  bnj1373  35450  bnj1489  35476  cvmliftlem10  35807  satfvsuc  35874  satfdm  35882  satf0suc  35889  sat1el2xp  35892  fmlasuc0  35897  satffunlem1lem1  35915  satffunlem2lem1  35917  mrexval  36014  mrsubffval  36020  msrval  36051  mthmpps  36095  lineunray  36660  rdgssun  38065  exrecfnlem  38066  finixpnum  38297  ptrest  38311  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem4  38316  poimirlem5  38317  poimirlem6  38318  poimirlem7  38319  poimirlem8  38320  poimirlem9  38321  poimirlem10  38322  poimirlem11  38323  poimirlem12  38324  poimirlem15  38327  poimirlem16  38328  poimirlem17  38329  poimirlem18  38330  poimirlem19  38331  poimirlem20  38332  poimirlem21  38333  poimirlem22  38334  poimirlem23  38335  poimirlem24  38336  poimirlem26  38338  poimirlem27  38339  poimirlem28  38340  poimirlem32  38344  mblfinlem2  38350  itg2addnclem2  38364  ecun  39083  ecuncnvepres  39085  ldualset  39940  paddval  40613  paddcom  40628  dvafset  41819  dvaset  41820  dvhfset  41895  dvhset  41896  hdmapfval  42642  hlhilset  42749  dvun  43161  fsuppssindlem2  43365  istopclsd  43472  fzsplit1nn0  43526  diophrw  43531  eldioph2lem1  43532  eldioph2lem2  43533  diophin  43544  diophren  43581  pwssplit4  43857  mendval  43947  iocunico  43979  tfsconcatun  44105  tfsconcat0i  44113  onsucunitp  44141  oaun3  44150  rclexi  44382  rtrclex  44384  rtrclexi  44388  cnvrcl0  44392  dfrtrcl5  44396  dfrcl2  44441  dfrcl3  44442  iunrelexp0  44469  trclfvdecomr  44495  dfrtrcl4  44505  frege131d  44531  clsk3nimkb  44807  clsk1indlem3  44810  clsk1independent  44813  ntrclskb  44836  ntrclsk3  44837  ntrclsk13  44838  permaxinf2lem  45762  dvmptfprodlem  46699  caratheodorylem1  47281  ovnsubadd2lem  47400  ovolval4lem1  47404  fzopredsuc  48102  clnbgrval  48628  cycl3grtri  48753  aacllem  50662