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

Theorem spc2gv 3136
 Description: Specialization with two quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.)
Hypothesis
Ref Expression
spc2egv.1
Assertion
Ref Expression
spc2gv
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)

Proof of Theorem spc2gv
StepHypRef Expression
1 spc2egv.1 . . . . 5
21notbid 296 . . . 4
32spc2egv 3135 . . 3
4 2nalexn 1699 . . 3
53, 4syl6ibr 231 . 2
65con4d 109 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wa 371  wal 1441   wceq 1443  wex 1662   wcel 1886 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-ext 2430 This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3046 This theorem is referenced by:  trel  4503  elovmpt2  6511  seqf1olem2  12250  seqf1o  12251  fi1uzind  12647  brfi1indALT  12650  pslem  16445  cnmpt12  20675  cnmpt22  20682  frg2woteqm  25780  mclsppslem  30214  mbfresfi  31980  lpolconN  35049  ismrcd2  35535  ismrc  35537
 Copyright terms: Public domain W3C validator