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

Theorem rspc2va 3217
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 3216 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A. x  e.  C  A. y  e.  D  ph  ->  ps ) )
43imp 427 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 367    = wceq 1398    e. wcel 1823   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-v 3108
This theorem is referenced by:  swopo  4799  soisores  6198  soisoi  6199  isocnv  6201  isotr  6207  ovrspc2v  6292  off  6527  caofrss  6546  caonncan  6551  wunpr  9076  injresinj  11907  seqcaopr2  12125  rlimcn2  13495  o1of2  13517  isprm6  14334  ssc2  15310  pospropd  15963  mndclOLD  16130  mndassOLD  16131  mhmpropd  16171  grpidssd  16313  grpinvssd  16314  isnsg3  16434  symgextf1  16645  efgredlemd  16961  efgredlem  16964  issrngd  17705  domneq0  18141  mplsubglem  18288  mplsubglemOLD  18290  lindfind  19018  lindsind  19019  mdetunilem1  19281  mdetunilem3  19283  mdetunilem4  19284  mdetunilem9  19289  decpmatmulsumfsupp  19441  pm2mpf1  19467  pm2mpmhmlem1  19486  t0sep  19992  tsmsxplem2  20822  comet  21182  nrmmetd  21261  tngngp  21334  reconnlem2  21498  iscmet3lem1  21896  iscmet3lem2  21897  dchrisumlem1  23872  pntpbnd1  23969  motcgr  24124  perpneq  24292  foot  24297  f1otrg  24376  axcontlem10  24478  frg2wot1  25259  tleile  27883  orngmul  28028  mndpluscn  28143  cvxscon  28952  elmrsubrn  29144  ghomco  30585  mzpcl34  30903  mgmhmpropd  32845  rnghmmul  32960
  Copyright terms: Public domain W3C validator