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

Theorem rspc2va 3187
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 3186 . 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 1370    e. wcel 1758   A.wral 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-v 3080
This theorem is referenced by:  swopo  4762  soisores  6130  soisoi  6131  isocnv  6133  isotr  6139  off  6447  caofrss  6466  caonncan  6471  wunpr  8990  injresinj  11759  seqcaopr2  11962  rlimcn2  13189  o1of2  13211  isprm6  13916  proplem2  14749  ssc2  14857  pospropd  15426  mhmpropd  15592  grpidssd  15724  grpinvssd  15725  isnsg3  15837  symgextf1  16048  efgredlemd  16365  efgredlem  16368  issrngd  17072  domneq0  17495  mplsubglem  17637  mplsubglemOLD  17639  mplcoe5lem  17674  lindfind  18373  lindsind  18374  mdetunilem1  18553  mdetunilem3  18555  mdetunilem4  18556  mdetunilem9  18561  t0sep  19063  tsmsxplem2  19863  comet  20223  nrmmetd  20302  tngngp  20375  reconnlem2  20539  iscmet3lem1  20937  iscmet3lem2  20938  dchrisumlem1  22874  pntpbnd1  22971  axcontlem10  23391  mndpluscn  26521  cvxscon  27296  ghomco  28916  mzpcl34  29235  frg2wot1  30818  decpmatmulsumfsupp  31280  pm2mpf1  31306  pm2mpmhmlem1  31325
  Copyright terms: Public domain W3C validator