Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  uneq12 Structured version   Unicode version

Theorem uneq12 3482
 Description: Equality theorem for union of two classes. (Contributed by NM, 29-Mar-1998.)
Assertion
Ref Expression
uneq12

Proof of Theorem uneq12
StepHypRef Expression
1 uneq1 3480 . 2
2 uneq2 3481 . 2
31, 2sylan9eq 2494 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 360   wceq 1653   cun 3304 This theorem is referenced by:  uneq12i  3485  uneq12d  3488  un00  3687  opthprc  4954  dmpropg  5372  unixp  5431  fntpg  5535  fnun  5580  resasplit  5642  fvun  5822  rankprb  7806  pm54.43  7918  xpscg  13814  ptuncnv  17870  evlseu  19968  sshjval  22883  diophun  26870  pwssplit4  27206 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-un 3311
 Copyright terms: Public domain W3C validator