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

Theorem rspc2va 3224
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 3223 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A. x  e.  C  A. y  e.  D  ph  ->  ps ) )
43imp 429 1  |-  ( ( ( A  e.  C  /\  B  e.  D
)  /\  A. x  e.  C  A. y  e.  D  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115
This theorem is referenced by:  swopo  4810  soisores  6212  soisoi  6213  isocnv  6215  isotr  6221  off  6539  caofrss  6558  caonncan  6563  wunpr  9088  injresinj  11895  seqcaopr2  12112  rlimcn2  13379  o1of2  13401  isprm6  14112  proplem2  14947  ssc2  15055  pospropd  15624  mhmpropd  15795  grpidssd  15928  grpinvssd  15929  isnsg3  16049  symgextf1  16260  efgredlemd  16577  efgredlem  16580  issrngd  17322  domneq0  17757  mplsubglem  17904  mplsubglemOLD  17906  mplcoe5lem  17941  lindfind  18658  lindsind  18659  mdetunilem1  18921  mdetunilem3  18923  mdetunilem4  18924  mdetunilem9  18929  decpmatmulsumfsupp  19081  pm2mpf1  19107  pm2mpmhmlem1  19126  t0sep  19631  tsmsxplem2  20483  comet  20843  nrmmetd  20922  tngngp  20995  reconnlem2  21159  iscmet3lem1  21557  iscmet3lem2  21558  dchrisumlem1  23499  pntpbnd1  23596  axcontlem10  24049  frg2wot1  24831  mndpluscn  27659  cvxscon  28439  elmrsubrn  28631  ghomco  30175  mzpcl34  30494  mgmcl  32152
  Copyright terms: Public domain W3C validator