Theorem uneq12d 3768

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

Syntax hints:   → wi 4   = wceq 1483   ∪ cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  symdifeq1  3846  csbun  4009  csbprg  4244  disjpr2  4248  disjpr2OLD  4249  diftpsn3  4332  diftpsn3OLD  4333  iunxprg  4607  rnpropg  5615  suceq  5790  fntpg  5948  foun  6155  f1oprswap  6180  fnimapr  6262  residpr  6409  fsnunfv  6453  fsnunres  6454  oarec  7642  ereq1  7749  mapunen  8129  cnfcomlem  8596  trcl  8604  r0weon  8835  infxpen  8837  cfsmolem  9092  cfsmo  9093  axdc3lem4  9275  ttukeylem3  9333  ttukey2g  9338  alephadd  9399  fpwwe2lem13  9464  wunex2  9560  wuncval2  9569  inar1  9597  prunioo  12301  fztp  12397  fzsuc2  12398  fseq1p1m1  12414  s3tpop  13654  s4dom  13664  trclun  13755  relexp0g  13762  relexpsucnnr  13765  dfrtrcl2  13802  setsvalg  15887  setsdm  15892  setsfun0  15894  setsid  15914  prdsval  16115  imasval  16171  mreexd  16302  mreexexlemd  16304  estrreslem2  16778  ipoval  17154  istsr  17217  gsumzaddlem  18321  pwssplit1  19059  psrval  19362  ordtval  20993  ordtcnv  21005  paste  21098  connsuba  21223  ptval2  21404  dfac14  21421  xkoptsub  21457  ptuncnv  21610  ptunhmeo  21611  xpstopnlem1  21612  alexsubALTlem3  21853  ustuqtop1  22045  rrxmvallem  23187  ovolioo  23336  uniiccdif  23346  itgsplitioo  23604  limcfval  23636  lhop2  23778  lgsquadlem2  25106  axlowdimlem13  25834  axlowdimlem15  25836  axlowdim  25841  eengv  25859  vtxdun  26377  trlsegvdeg  27087  ex-res  27298  imadifxp  29414  funresdm1  29416  padct  29497  resf1o  29505  ordtprsval  29964  ordtprsuni  29965  ordtcnvNEW  29966  unelcarsg  30374  carsgclctunlem1  30379  eulerpartlemt  30433  sseqval  30450  probun  30481  bnj1373  31098  bnj1489  31124  cvmliftlem10  31276  mrexval  31398  mrsubffval  31404  msrval  31435  mthmpps  31479  nodenselem5  31838  nosupbnd2lem1  31861  nosupbnd2  31862  lineunray  32254  finixpnum  33394  ptrest  33408  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem32  33441  mblfinlem2  33447  itg2addnclem2  33462  ldualset  34412  paddval  35084  paddcom  35099  dvafset  36292  dvaset  36293  dvhfset  36369  dvhset  36370  hdmapfval  37119  hlhilset  37226  istopclsd  37263  fzsplit1nn0  37317  diophrw  37322  eldioph2lem1  37323  eldioph2lem2  37324  diophin  37336  diophren  37377  pwssplit4  37659  mendval  37753  iocunico  37796  rclexi  37922  rtrclex  37924  rtrclexi  37928  cnvrcl0  37932  dfrtrcl5  37936  dfrcl2  37966  dfrcl3  37967  iunrelexp0  37994  trclfvdecomr  38020  dfrtrcl4  38030  frege131d  38056  clsk3nimkb  38338  clsk1indlem3  38341  clsk1independent  38344  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  dvmptfprodlem  40159  caratheodorylem1  40740  ovnsubadd2lem  40859  ovolval4lem1  40863  fzopredsuc  41333  xpprsng  42110  mndpsuppss  42152  aacllem  42547