Theorem uneq2d 4141

Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)

Hypothesis

Ref	Expression
uneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
uneq2d	⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

Proof of Theorem uneq2d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq2 4135	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	syl 17	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:  ifeq2  4474  tpeq3  4682  iununi  5023  sucprc  6268  resasplit  6550  fvun1  6756  fmptapd  6935  fndifnfp  6940  fvunsn  6943  fnsnsplit  6948  oev2  8150  oarec  8190  ralxpmap  8462  sbthlem5  8633  sbthlem6  8634  domss2  8678  domunfican  8793  fiint  8797  fodomfi  8799  pm54.43  9431  kmlem2  9579  kmlem11  9588  ackbij1lem1  9644  fin23lem26  9749  axdc3lem4  9877  fpwwe2lem13  10066  wunex2  10162  wuncval2  10171  ioounsn  12866  snunico  12868  ioojoin  12872  fzsuc  12957  fseq1p1m1  12984  fseq1m1p1  12985  fzosplitsnm1  13115  fzosplitsn  13148  fzosplitpr  13149  fzosplitprm1  13150  hashfun  13801  resunimafz0  13806  s4prop  14274  fsumm1  15108  climcndslem1  15206  fprodm1  15323  ruclem4  15589  lcmfunsnlem1  15983  lcmfunsnlem2lem1  15984  lcmfunsnlem2lem2  15985  lcmfunsnlem2  15986  lcmfunsn  15990  vdwap1  16315  setsidvald  16516  setscom  16529  mreexmrid  16916  mreexexlemd  16917  mreexexlem2d  16918  cnvtsr  17834  dprd2da  19166  dmdprdsplit2lem  19169  lspun0  19785  lbsextlem4  19935  cmpcld  22012  comppfsc  22142  trfil2  22497  cldsubg  22721  tsmsres  22754  icccmplem2  23433  uniioombllem4  24189  ppiprm  25730  chtprm  25732  pntrsumbnd2  26145  pthdlem1  27549  wwlksnext  27673  clwwlknonex2lem1  27888  iunxunsn  30320  iunxunpr  30321  difres  30352  ofpreima2  30413  fzspl  30515  tocyc01  30762  ordtprsuni  31164  ordtcnvNEW  31165  carsgsigalem  31575  ballotlemfp1  31751  fsum2dsub  31880  reprsuc  31888  bnj941  32046  bnj944  32212  subfacp1lem1  32428  cvmscld  32522  satf  32602  satfv1  32612  fmlasuc  32635  mrsubvrs  32771  mclsval  32812  noextend  33175  nodenselem5  33194  nosupbnd2lem1  33217  rankaltopb  33442  rankung  33629  lindsadd  34887  lindsenlbs  34889  poimirlem1  34895  poimirlem2  34896  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem13  34907  poimirlem14  34908  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem26  34920  poimirlem28  34922  poimirlem31  34925  poimirlem32  34926  lshpnel2N  36123  paddfval  36935  hdmapval  38966  diophren  39417  iunrelexp0  40054  trclfvdecoml  40081  isotone1  40405  iunp1  41335  snunioo1  41795  dvmptfprodlem  42236  stoweidlem11  42303  stoweidlem26  42318  fourierdlem33  42432  fzopredsuc  43530  iccpartltu  43592  iccpartgt  43594  lmod1zr  44555