MPE Home 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  |-  ( ( x  =  A  /\  y  =  B )  ->  ( ph  <->  ps )
)
Assertion
Ref Expression
spc2gv  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A. x A. y ph  ->  ps )
)
Distinct variable groups:    x, y, A    x, B, y    ps, x, y
Allowed substitution hints:    ph( x, y)    V( x, y)    W( x, y)

Proof of Theorem spc2gv
StepHypRef Expression
1 spc2egv.1 . . . . 5  |-  ( ( x  =  A  /\  y  =  B )  ->  ( ph  <->  ps )
)
21notbid 296 . . . 4  |-  ( ( x  =  A  /\  y  =  B )  ->  ( -.  ph  <->  -.  ps )
)
32spc2egv 3135 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( -.  ps  ->  E. x E. y  -. 
ph ) )
4 2nalexn 1699 . . 3  |-  ( -. 
A. x A. y ph 
<->  E. x E. y  -.  ph )
53, 4syl6ibr 231 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( -.  ps  ->  -. 
A. x A. y ph ) )
65con4d 109 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A. x A. y ph  ->  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371   A.wal 1441    = wceq 1443   E.wex 1662    e. 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