Theorem uneq2d 4122

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 4116	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

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

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 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911

This theorem is used by:  ifeq2  4494  tpeq3  4712  iununi  5067  sucprc  6443  unisucs  6444  resasplit  6752  fvun1  6976  fmptapd  7175  fndifnfp  7180  fvunsn  7183  fnsnsplit  7188  f1ofvswap  7313  oev2  8514  oarec  8553  ralxpmap  8900  sbthlem5  9086  sbthlem6  9087  domss2  9131  dif1en  9153  unfi  9162  fodomfi  9279  domunfican  9288  fiint  9293  pm54.43  10003  kmlem2  10151  kmlem11  10160  ackbij1lem1  10218  fin23lem26  10324  axdc3lem4  10452  fpwwe2lem12  10644  wunex2  10740  wuncval2  10749  indconst1  12248  ioounsn  13522  snunico  13524  ioojoin  13528  fzsuc  13618  fseq1p1m1  13645  fseq1m1p1  13646  fzosplitsnm1  13788  fzosplitsn  13824  fzosplitpr  13825  fzosplitprm1  13826  hashfun  14494  resunimafz0  14502  s4prop  14973  fsumm1  15827  climcndslem1  15928  fprodm1  16046  ruclem4  16314  lcmfunsnlem1  16719  lcmfunsnlem2lem1  16720  lcmfunsnlem2lem2  16721  lcmfunsnlem2  16722  lcmfunsn  16726  vdwap1  17061  setscom  17264  setsidvald  17283  mreexmrid  17723  mreexexlemd  17724  mreexexlem2d  17725  cnvtsr  18668  dprd2da  20160  dmdprdsplit2lem  20163  lspun0  21184  lbsextlem4  21337  cmpcld  23611  comppfsc  23742  trfil2  24097  cldsubg  24321  tsmsres  24354  icccmplem2  25034  uniioombllem4  25798  ppiprm  27368  chtprm  27370  pntrsumbnd2  27784  noextend  27883  nodenselem5  27905  nosupbnd2lem1  27932  addsproplem1  28215  addsprop  28222  negsproplem1  28274  negsprop  28281  mulsproplemcbv  28361  mulsproplem1  28362  mulsprop  28376  precsexlemcbv  28452  precsexlem3  28455  onleft  28506  ltonold  28507  oncutlt  28510  pthdlem1  30181  wwlksnext  30311  clwwlknonex2lem1  30527  iunxunsn  32984  iunxunpr  32985  difres  33018  ofpreima2  33084  fzspl  33206  tocyc01  33504  esplyind  34031  ordtprsuni  34375  ordtcnvNEW  34376  carsgsigalem  34772  ballotlemfp1  34949  fsum2dsub  35061  reprsuc  35069  bnj941  35228  bnj944  35393  fineqvac  35588  subfacp1lem1  35710  cvmscld  35804  satf  35884  satfv1  35894  fmlasuc  35917  mrsubvrs  36053  mclsval  36094  rankaltopb  36510  rankung  36697  lindsadd  38323  lindsenlbs  38325  poimirlem1  38331  poimirlem2  38332  poimirlem4  38334  poimirlem6  38336  poimirlem7  38337  poimirlem8  38338  poimirlem13  38343  poimirlem14  38344  poimirlem16  38346  poimirlem17  38347  poimirlem18  38348  poimirlem19  38349  poimirlem20  38350  poimirlem21  38351  poimirlem22  38352  poimirlem26  38356  poimirlem28  38358  poimirlem31  38361  poimirlem32  38362  lshpnel2N  39819  paddfval  40631  hdmapval  42662  fzsplitnd  42809  lcmfunnnd  42839  fsuppssind  43385  diophren  43600  omabs2  44119  tfsconcatrn  44129  tfsconcatrev  44135  iunrelexp0  44488  trclfvdecoml  44515  isotone1  44834  iunp1  45846  snunioo1  46288  dvmptfprodlem  46718  stoweidlem11  46785  stoweidlem26  46800  fourierdlem33  46914  fzopredsuc  48121  iccpartltu  48234  iccpartgt  48236  dfclnbgr2  48648  dfclnbgr4  48649  dfclnbgr3  48651  clnbupgr  48658  clnbgr0edg  48662  dfclnbgr5  48675  dfclnbgr6  48681  dfsclnbgr6  48683  cycl3grtri  48772  stgrclnbgr0  48790  lmod1zr  49332  tposres2  49717