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

Theorem rspc2va 3220
Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)
Hypotheses
Ref Expression
rspc2v.1
rspc2v.2
Assertion
Ref Expression
rspc2va
Distinct variable groups:   , ,   ,   ,   , ,   ,   ,

Proof of Theorem rspc2va
StepHypRef Expression
1 rspc2v.1 . . 3
2 rspc2v.2 . . 3
31, 2rspc2v 3219 . 2
43imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807
This theorem is referenced by:  swopo  4815  soisores  6223  soisoi  6224  isocnv  6226  isotr  6232  ovrspc2v  6318  off  6554  caofrss  6573  caonncan  6578  wunpr  9108  injresinj  11926  seqcaopr2  12143  rlimcn2  13413  o1of2  13435  isprm6  14250  ssc2  15191  pospropd  15764  mndclOLD  15931  mndassOLD  15932  mhmpropd  15972  grpidssd  16114  grpinvssd  16115  isnsg3  16235  symgextf1  16446  efgredlemd  16762  efgredlem  16765  issrngd  17510  domneq0  17946  mplsubglem  18093  mplsubglemOLD  18095  lindfind  18851  lindsind  18852  mdetunilem1  19114  mdetunilem3  19116  mdetunilem4  19117  mdetunilem9  19122  decpmatmulsumfsupp  19274  pm2mpf1  19300  pm2mpmhmlem1  19319  t0sep  19825  tsmsxplem2  20656  comet  21016  nrmmetd  21095  tngngp  21168  reconnlem2  21332  iscmet3lem1  21730  iscmet3lem2  21731  dchrisumlem1  23674  pntpbnd1  23771  motcgr  23923  perpneq  24091  foot  24096  f1otrg  24174  axcontlem10  24276  frg2wot1  25057  tleile  27649  orngmul  27793  mndpluscn  27908  cvxscon  28688  elmrsubrn  28880  ghomco  30345  mzpcl34  30663  mgmhmpropd  32473  rnghmmul  32706
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-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-ral 2812  df-v 3111
  Copyright terms: Public domain W3C validator