Theorem uneq12d 4142

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

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943

This theorem is referenced by:  symdifeq1  4223  csbun  4392  csbprg  4647  disjpr2  4651  diftpsn3  4737  iunxprg  5020  rnpropg  6081  suceq  6258  fntpg  6416  foun  6635  f1oprswap  6660  fnimapr  6749  xpprsng  6904  residpr  6907  fvsnun2  6947  fsnunfv  6951  fsnunres  6952  oarec  8190  ereq1  8298  mapunen  8688  cnfcomlem  9164  trcl  9172  djueq12  9335  r0weon  9440  infxpen  9442  cfsmolem  9694  cfsmo  9695  axdc3lem4  9877  ttukeylem3  9935  ttukey2g  9940  alephadd  10001  fpwwe2lem13  10066  wunex2  10162  wuncval2  10171  inar1  10199  prunioo  12870  fztp  12966  fzsuc2  12968  fseq1p1m1  12984  s3tpop  14273  s4dom  14283  trclun  14376  relexp0g  14383  relexpsucnnr  14386  dfrtrcl2  14423  setsvalg  16514  setsdm  16519  setsfun0  16521  setsid  16540  prdsval  16730  imasval  16786  mreexd  16915  mreexexlemd  16917  estrreslem2  17390  ipoval  17766  istsr  17829  gsumzaddlem  19043  pwssplit1  19833  psrval  20144  ordtval  21799  ordtcnv  21811  paste  21904  connsuba  22030  ptval2  22211  dfac14  22228  xkoptsub  22264  ptuncnv  22417  ptunhmeo  22418  xpstopnlem1  22419  alexsubALTlem3  22659  ustuqtop1  22852  rrxmvallem  24009  ovolioo  24171  uniiccdif  24181  itgsplitioo  24440  limcfval  24472  lhop2  24614  lgsquadlem2  25959  axlowdimlem13  26742  axlowdimlem15  26744  axlowdim  26749  eengv  26767  vtxdun  27265  trlsegvdeg  28008  numclwwlk3lem2lem  28164  ex-res  28222  imadifxp  30353  funresdm1  30357  fnimatp  30425  cnvprop  30434  mptprop  30436  coprprop  30437  padct  30457  resf1o  30468  symgcom  30729  tocycfv  30753  tocycf  30761  tocyc01  30762  cycpm2tr  30763  cycpmco2f1  30768  cycpmco2rn  30769  cycpmconjv  30786  cycpmconjslem2  30799  ordtprsval  31163  ordtprsuni  31164  ordtcnvNEW  31165  unelcarsg  31572  carsgclctunlem1  31577  eulerpartlemt  31631  sseqval  31648  probun  31679  bnj1373  32304  bnj1489  32330  cvmliftlem10  32543  satfvsuc  32610  satfdm  32618  satf0suc  32625  sat1el2xp  32628  fmlasuc0  32633  satffunlem1lem1  32651  satffunlem2lem1  32653  mrexval  32750  mrsubffval  32756  msrval  32787  mthmpps  32831  frrlem12  33136  nodenselem5  33194  nosupbnd2lem1  33217  nosupbnd2  33218  lineunray  33610  rdgssun  34661  exrecfnlem  34662  finixpnum  34879  ptrest  34893  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem9  34903  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem23  34917  poimirlem24  34918  poimirlem26  34920  poimirlem27  34921  poimirlem28  34922  poimirlem32  34926  mblfinlem2  34932  itg2addnclem2  34946  ldualset  36263  paddval  36936  paddcom  36951  dvafset  38142  dvaset  38143  dvhfset  38218  dvhset  38219  hdmapfval  38965  hlhilset  39072  istopclsd  39304  fzsplit1nn0  39358  diophrw  39363  eldioph2lem1  39364  eldioph2lem2  39365  diophin  39376  diophren  39417  pwssplit4  39696  mendval  39790  iocunico  39824  rclexi  39982  rtrclex  39984  rtrclexi  39988  cnvrcl0  39992  dfrtrcl5  39996  dfrcl2  40026  dfrcl3  40027  iunrelexp0  40054  trclfvdecomr  40080  dfrtrcl4  40090  frege131d  40116  clsk3nimkb  40397  clsk1indlem3  40400  clsk1independent  40403  ntrclskb  40426  ntrclsk3  40427  ntrclsk13  40428  dvmptfprodlem  42236  caratheodorylem1  42815  ovnsubadd2lem  42934  ovolval4lem1  42938  fzopredsuc  43530  mndpsuppss  44426  aacllem  44909