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

Theorem rspc2va 2976
Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)
Hypotheses
Ref Expression
rspc2v.1  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
rspc2v.2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
Assertion
Ref Expression
rspc2va  |-  ( ( ( A  e.  C  /\  B  e.  D
)  /\  A. x  e.  C  A. y  e.  D  ph )  ->  ps )
Distinct variable groups:    x, y, A    y, B    x, C    x, D, y    ch, x    ps, y
Allowed substitution hints:    ph( x, y)    ps( x)    ch( y)    B( x)    C( y)

Proof of Theorem rspc2va
StepHypRef Expression
1 rspc2v.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
2 rspc2v.2 . . 3  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
31, 2rspc2v 2975 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A. x  e.  C  A. y  e.  D  ph  ->  ps ) )
43imp 418 1  |-  ( ( ( A  e.  C  /\  B  e.  D
)  /\  A. x  e.  C  A. y  e.  D  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1647    e. wcel 1715   A.wral 2628
This theorem is referenced by:  swopo  4427  soisores  5947  soisoi  5948  isocnv  5950  isotr  5956  off  6220  caofrss  6237  caonncan  6242  wunpr  8478  injresinj  11087  seqcaopr2  11246  rlimcn2  12271  o1of2  12293  isprm6  12996  proplem2  13801  ssc2  13909  pospropd  14448  mhmpropd  14631  isnsg3  14861  efgredlemd  15263  efgredlem  15266  issrngd  15836  domneq0  16248  mplsubglem  16389  t0sep  17269  tsmsxplem2  18049  comet  18272  nrmmetd  18310  tngngp  18383  reconnlem2  18546  iscmet3lem1  18932  iscmet3lem2  18933  dchrisumlem1  20861  pntpbnd1  20958  off2  23457  mndpluscn  23667  ofcf  23951  cvxscon  24377  axcontlem10  25343  ghomco  26079  mzpcl34  26315  lindfind  26792  lindsind  26793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ral 2633  df-v 2875
  Copyright terms: Public domain W3C validator