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

Theorem uneq12i 3655
Description: Equality inference for union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
uneq1i.1
uneq12i.2
Assertion
Ref Expression
uneq12i

Proof of Theorem uneq12i
StepHypRef Expression
1 uneq1i.1 . 2
2 uneq12i.2 . 2
3 uneq12 3652 . 2
41, 2, 3mp2an 672 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  u.cun 3473
This theorem is referenced by:  indir  3745  difundir  3750  difindi  3751  symdif1  3762  unrab  3768  rabun2  3776  dfif6  3944  dfif3  3955  dfif5  3957  unopab  4527  xpundi  5057  xpundir  5058  xpun  5062  dmun  5214  resundi  5292  resundir  5293  cnvun  5416  rnun  5419  imaundi  5423  imaundir  5424  dmtpop  5489  coundi  5513  coundir  5514  unidmrn  5542  dfdm2  5544  mptun  5717  resasplit  5760  fresaun  5761  fresaunres2  5762  residpr  6075  fpr  6079  fvsnun2  6107  sbthlem5  7651  1sdom  7742  cdaassen  8583  fzo0to42pr  11901  hashgval  12408  hashinf  12410  vdwlem6  14504  setsres  14660  xpsc  14954  lefld  15856  opsrtoslem1  18148  volun  21955  iblcnlem1  22194  usgraexvlem  24395  ex-dif  25144  ex-in  25146  ex-pw  25150  ex-xp  25157  ex-cnv  25158  ex-rn  25161  partfun  27516  ordtprsuni  27901  indval2  28028  sigaclfu2  28121  eulerpartgbij  28311  subfacp1lem1  28623  subfacp1lem5  28628  predun  29270  symdif0  29474  symdifid  29476  fixun  29559  bpoly3  29820  onint1  29914  itg2addnclem2  30067  iblabsnclem  30078  refssfne  30176  rnfdmpr  32308  bj-pr1un  34561  bj-pr21val  34571  bj-pr2un  34575  bj-pr22val  34577
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
  Copyright terms: Public domain W3C validator