Theorem uneq12d 4140

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

Syntax hints:   → wi 4   = wceq 1533   ∪ cun 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3941

This theorem is referenced by:  symdifeq1  4221  csbun  4390  csbprg  4639  disjpr2  4643  diftpsn3  4729  iunxprg  5011  rnpropg  6074  suceq  6251  fntpg  6409  foun  6628  f1oprswap  6653  fnimapr  6742  xpprsng  6897  residpr  6900  fvsnun2  6940  fsnunfv  6944  fsnunres  6945  oarec  8182  ereq1  8290  mapunen  8680  cnfcomlem  9156  trcl  9164  djueq12  9327  r0weon  9432  infxpen  9434  cfsmolem  9686  cfsmo  9687  axdc3lem4  9869  ttukeylem3  9927  ttukey2g  9932  alephadd  9993  fpwwe2lem13  10058  wunex2  10154  wuncval2  10163  inar1  10191  prunioo  12861  fztp  12957  fzsuc2  12959  fseq1p1m1  12975  s3tpop  14265  s4dom  14275  trclun  14368  relexp0g  14375  relexpsucnnr  14378  dfrtrcl2  14415  setsvalg  16506  setsdm  16511  setsfun0  16513  setsid  16532  prdsval  16722  imasval  16778  mreexd  16907  mreexexlemd  16909  estrreslem2  17382  ipoval  17758  istsr  17821  gsumzaddlem  19035  pwssplit1  19825  psrval  20136  ordtval  21791  ordtcnv  21803  paste  21896  connsuba  22022  ptval2  22203  dfac14  22220  xkoptsub  22256  ptuncnv  22409  ptunhmeo  22410  xpstopnlem1  22411  alexsubALTlem3  22651  ustuqtop1  22844  rrxmvallem  24001  ovolioo  24163  uniiccdif  24173  itgsplitioo  24432  limcfval  24464  lhop2  24606  lgsquadlem2  25951  axlowdimlem13  26734  axlowdimlem15  26736  axlowdim  26741  eengv  26759  vtxdun  27257  trlsegvdeg  28000  numclwwlk3lem2lem  28156  ex-res  28214  imadifxp  30345  funresdm1  30349  fnimatp  30417  cnvprop  30426  mptprop  30428  coprprop  30429  padct  30449  resf1o  30460  symgcom  30722  tocycfv  30746  tocycf  30754  tocyc01  30755  cycpm2tr  30756  cycpmco2f1  30761  cycpmco2rn  30762  cycpmconjv  30779  cycpmconjslem2  30792  ordtprsval  31156  ordtprsuni  31157  ordtcnvNEW  31158  unelcarsg  31565  carsgclctunlem1  31570  eulerpartlemt  31624  sseqval  31641  probun  31672  bnj1373  32297  bnj1489  32323  cvmliftlem10  32536  satfvsuc  32603  satfdm  32611  satf0suc  32618  sat1el2xp  32621  fmlasuc0  32626  satffunlem1lem1  32644  satffunlem2lem1  32646  mrexval  32743  mrsubffval  32749  msrval  32780  mthmpps  32824  frrlem12  33129  nodenselem5  33187  nosupbnd2lem1  33210  nosupbnd2  33211  lineunray  33603  rdgssun  34653  exrecfnlem  34654  finixpnum  34871  ptrest  34885  poimirlem1  34887  poimirlem2  34888  poimirlem3  34889  poimirlem4  34890  poimirlem5  34891  poimirlem6  34892  poimirlem7  34893  poimirlem8  34894  poimirlem9  34895  poimirlem10  34896  poimirlem11  34897  poimirlem12  34898  poimirlem15  34901  poimirlem16  34902  poimirlem17  34903  poimirlem18  34904  poimirlem19  34905  poimirlem20  34906  poimirlem21  34907  poimirlem22  34908  poimirlem23  34909  poimirlem24  34910  poimirlem26  34912  poimirlem27  34913  poimirlem28  34914  poimirlem32  34918  mblfinlem2  34924  itg2addnclem2  34938  ldualset  36255  paddval  36928  paddcom  36943  dvafset  38134  dvaset  38135  dvhfset  38210  dvhset  38211  hdmapfval  38957  hlhilset  39064  istopclsd  39290  fzsplit1nn0  39344  diophrw  39349  eldioph2lem1  39350  eldioph2lem2  39351  diophin  39362  diophren  39403  pwssplit4  39682  mendval  39776  iocunico  39810  rclexi  39968  rtrclex  39970  rtrclexi  39974  cnvrcl0  39978  dfrtrcl5  39982  dfrcl2  40012  dfrcl3  40013  iunrelexp0  40040  trclfvdecomr  40066  dfrtrcl4  40076  frege131d  40102  clsk3nimkb  40383  clsk1indlem3  40386  clsk1independent  40389  ntrclskb  40412  ntrclsk3  40413  ntrclsk13  40414  dvmptfprodlem  42221  caratheodorylem1  42801  ovnsubadd2lem  42920  ovolval4lem1  42924  fzopredsuc  43516  mndpsuppss  44412  aacllem  44895