Theorem uneq2d 4166

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∪ cun 4148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150

This theorem is used by:  ifeq2  4486  tpeq3  4701  iununi  5058  sucprc  6444  unisucs  6445  resasplit  6757  fvun1  6981  fmptapd  7180  fndifnfp  7185  fvunsn  7188  fnsnsplit  7193  f1ofvswap  7318  oev2  8539  oarec  8578  ralxpmap  8932  sbthlem5  9118  sbthlem6  9119  domss2  9163  dif1en  9185  unfi  9194  fodomfi  9312  domunfican  9321  fiint  9326  rankung  9880  pm54.43  10089  kmlem2  10237  kmlem11  10246  ackbij1lem1  10304  fin23lem26  10410  axdc3lem4  10538  fpwwe2lem12  10734  wunex2  10830  wuncval2  10839  indconst1  12340  ioounsn  13615  snunico  13617  ioojoin  13621  fzsuc  13712  fseq1p1m1  13739  fseq1m1p1  13740  fzosplitsnm1  13882  fzosplitsn  13918  fzosplitpr  13919  fzosplitprm1  13920  hashfun  14589  resunimafz0  14597  s4prop  15070  fsumm1  15926  climcndslem1  16027  fprodm1  16143  ruclem4  16411  lcmfunsnlem1  16821  lcmfunsnlem2lem1  16822  lcmfunsnlem2lem2  16823  lcmfunsnlem2  16824  lcmfunsn  16828  vdwap1  17164  setscom  17367  setsidvald  17386  mreexmrid  17826  mreexexlemd  17827  mreexexlem2d  17828  cnvtsr  18771  dprd2da  20267  dmdprdsplit2lem  20270  lspun0  21295  lbsextlem4  21448  lindsenlbs  22166  cmpcld  23729  comppfsc  23860  trfil2  24215  cldsubg  24439  tsmsres  24472  icccmplem2  25152  uniioombllem4  25916  ppiprm  27487  chtprm  27489  pntrsumbnd2  27903  noextend  28032  nodenselem5  28054  nosupbnd2lem1  28081  addsproplem1  28364  addsprop  28371  negsproplem1  28423  negsprop  28430  mulsproplemcbv  28510  mulsproplem1  28511  mulsprop  28525  precsexlemcbv  28601  precsexlem3  28604  onleft  28655  ltonold  28656  oncutlt  28659  pthdlem1  30361  wwlksnext  30491  clwwlknonex2lem1  30707  iunxunsn  33211  iunxunpr  33212  difres  33245  ofpreima2  33311  fzspl  33431  tocyc01  33729  esplyind  34257  ordtprsuni  34601  ordtcnvNEW  34602  carsgsigalem  34997  ballotlemfp1  35174  fsum2dsub  35286  reprsuc  35294  bnj941  35453  bnj944  35618  fineqvac  35852  subfacp1lem1  36062  cvmscld  36156  satf  36236  satfv1  36246  fmlasuc  36269  mrsubvrs  36405  mclsval  36446  rankaltopb  36868  lindsadd  38673  poimirlem1  38676  poimirlem2  38677  poimirlem4  38679  poimirlem6  38681  poimirlem7  38682  poimirlem8  38683  poimirlem13  38688  poimirlem14  38689  poimirlem16  38691  poimirlem17  38692  poimirlem18  38693  poimirlem19  38694  poimirlem20  38695  poimirlem21  38696  poimirlem22  38697  poimirlem26  38701  poimirlem28  38703  poimirlem31  38706  poimirlem32  38707  lshpnel2N  40179  paddfval  40991  hdmapval  43022  fzsplitnd  43169  lcmfunnnd  43199  fsuppssind  43758  diophren  43957  omabs2  44471  tfsconcatrn  44481  tfsconcatrev  44487  iunrelexp0  44839  trclfvdecoml  44866  isotone1  45185  iunp1  46219  snunioo1  46660  dvmptfprodlem  47090  stoweidlem11  47157  stoweidlem26  47172  fourierdlem33  47286  fzopredsuc  48530  iccpartltu  48643  iccpartgt  48645  dfclnbgr2  49057  dfclnbgr4  49058  dfclnbgr3  49060  clnbupgr  49067  clnbgr0edg  49071  dfclnbgr5  49084  dfclnbgr6  49090  dfsclnbgr6  49092  cycl3grtri  49181  stgrclnbgr0  49199  lmod1zr  49741  tposres2  50129