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

Theorem rspc2va 3027
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 3026 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A. x  e.  C  A. y  e.  D  ph  ->  ps ) )
43imp 419 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 177    /\ wa 359    = wceq 1649    e. wcel 1721   A.wral 2674
This theorem is referenced by:  swopo  4481  soisores  6014  soisoi  6015  isocnv  6017  isotr  6023  off  6287  caofrss  6304  caonncan  6309  wunpr  8548  injresinj  11163  seqcaopr2  11322  rlimcn2  12347  o1of2  12369  isprm6  13072  proplem2  13877  ssc2  13985  pospropd  14524  mhmpropd  14707  isnsg3  14937  efgredlemd  15339  efgredlem  15342  issrngd  15912  domneq0  16320  mplsubglem  16461  t0sep  17350  tsmsxplem2  18144  comet  18504  nrmmetd  18583  tngngp  18656  reconnlem2  18819  iscmet3lem1  19205  iscmet3lem2  19206  dchrisumlem1  21144  pntpbnd1  21241  mndpluscn  24273  cvxscon  24891  axcontlem10  25824  ghomco  26456  mzpcl34  26686  lindfind  27162  lindsind  27163  frg2wot1  28168
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ral 2679  df-v 2926
  Copyright terms: Public domain W3C validator