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

Theorem rspc2va 2891
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 2890 . 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 1623    e. wcel 1684   A.wral 2543
This theorem is referenced by:  swopo  4324  soisores  5824  soisoi  5825  isocnv  5827  isotr  5833  off  6093  caofrss  6110  caonncan  6115  wunpr  8331  seqcaopr2  11082  rlimcn2  12064  o1of2  12086  isprm6  12788  proplem2  13591  ssc2  13699  pospropd  14238  mhmpropd  14421  isnsg3  14651  efgredlemd  15053  efgredlem  15056  issrngd  15626  domneq0  16038  mplsubglem  16179  t0sep  17052  tsmsxplem2  17836  comet  18059  nrmmetd  18097  tngngp  18170  reconnlem2  18332  iscmet3lem1  18717  iscmet3lem2  18718  dchrisumlem1  20638  pntpbnd1  20735  off2  23208  mndpluscn  23299  ofcf  23464  cvxscon  23774  axcontlem10  24601  isig2a2  26066  ghomco  26573  mzpcl34  26809  lindfind  27286  lindsind  27287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790
  Copyright terms: Public domain W3C validator