Theorem uneq2i 3654

Description: Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
uneq1i.1

Assertion

Ref	Expression
uneq2i

Proof of Theorem uneq2i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2
2		uneq2 3651	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  u.cun 3473

This theorem is referenced by:  un4  3663  unundir  3665  difdif2  3754  difun2  3907  difdifdir  3915  dfif5  3957  qdass  4129  qdassr  4130  ssunpr  4192  iununi  4415  unidif0  4625  unisuc  4959  iunsuc  4965  difxp1  5437  fresaun  5761  fresaunres2  5762  fvssunirn  5894  fmptap  6094  fvsnun1  6106  funiunfv  6160  onuninsuci  6675  tfrlem10  7075  oarec  7230  dfdom2  7561  fodomr  7688  dfsup3OLD  7924  ranksuc  8304  kmlem3  8553  fin1a2lem10  8810  fin1a2lem12  8812  axdc3lem4  8854  prunioo  11678  facnn  12355  fac0  12356  hashun3  12452  fsum2dlem  13585  fsumiun  13635  incexclem  13648  fprod2dlem  13784  prmreclem4  14437  strlemor1  14724  strlemor2  14725  strlemor3  14726  phlstr  14778  mreexexlem4d  15044  opsrtoslem2  18149  restcld  19673  neitr  19681  fiuncmp  19904  refun0  20016  1stckgenlem  20054  filcon  20384  ufildr  20432  alexsubALTlem3  20549  ptcmplem1  20552  restmetu  21090  ovolfiniun  21912  unmbl  21948  volfiniun  21957  voliunlem1  21960  plyun0  22594  lgsquadlem3  23631  axlowdimlem3  24247  axlowdimlem17  24261  usgrafilem1  24411  constr3trllem3  24652  constr3pthlem1  24655  ex-un  25145  ex-pw  25150  iuninc  27428  difico  27594  subfacp1lem1  28623  cvmliftlem10  28739  wfrlem13  29355  wfrlem14  29356  wfrlem16  29358  mbfresfi  30061  asindmre  30102  mapfzcons  30648  mapfzcons1  30649  diophin  30706  iocunico  31178  fourierdlem65  31954  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem100  31989  fourierdlem105  31994  fourierdlem108  31997  fourierdlem109  31998  fourierdlem110  31999  fourierdlem112  32001  fourierdlem113  32002  lmod1zr  33094  bnj601  33978  bnj1416  34095  rp-fakeuninass  37741  trclubg  37785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480