Theorem uneq2 3651

Description: Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
uneq2

Proof of Theorem uneq2

Step	Hyp	Ref	Expression
1		uneq1 3650	. 2
2		uncom 3647	. 2
3		uncom 3647	. 2
4	1, 2, 3	3eqtr4g 2523	1

Syntax hints:  ->wi 4  =wceq 1395  u.cun 3473

This theorem is referenced by:  uneq12  3652  uneq2i  3654  uneq2d  3657  uneqin  3748  disjssun  3884  uniprg  4263  sucprc  4958  unexb  6600  undifixp  7525  unxpdom  7747  ackbij1lem16  8636  fin23lem28  8741  ttukeylem6  8915  ipodrsima  15795  mplsubglem  18093  mplsubglemOLD  18095  mretopd  19593  iscldtop  19596  dfcon2  19920  nconsubb  19924  comppfsc  20033  spanun  26463  locfinref  27844  nofulllem1  29462  brsuccf  29591  rankung  29823  nacsfix  30644  eldioph4b  30745  eldioph4i  30746  fiuneneq  31154  paddval  35522  dochsatshp  37178

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