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

Theorem rspc2va 3059
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 3058 . 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 1652    e. wcel 1725   A.wral 2705
This theorem is referenced by:  swopo  4513  soisores  6047  soisoi  6048  isocnv  6050  isotr  6056  off  6320  caofrss  6337  caonncan  6342  wunpr  8584  injresinj  11200  seqcaopr2  11359  rlimcn2  12384  o1of2  12406  isprm6  13109  proplem2  13914  ssc2  14022  pospropd  14561  mhmpropd  14744  isnsg3  14974  efgredlemd  15376  efgredlem  15379  issrngd  15949  domneq0  16357  mplsubglem  16498  t0sep  17388  tsmsxplem2  18183  comet  18543  nrmmetd  18622  tngngp  18695  reconnlem2  18858  iscmet3lem1  19244  iscmet3lem2  19245  dchrisumlem1  21183  pntpbnd1  21280  mndpluscn  24312  cvxscon  24930  axcontlem10  25912  ghomco  26558  mzpcl34  26788  lindfind  27263  lindsind  27264  frg2wot1  28446
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-v 2958
  Copyright terms: Public domain W3C validator