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

Theorem rspc2v 2890
Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)
Hypotheses
Ref Expression
rspc2v.1  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
rspc2v.2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
Assertion
Ref Expression
rspc2v  |-  ( ( 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 rspc2v
StepHypRef Expression
1 nfv 1605 . 2  |-  F/ x ch
2 nfv 1605 . 2  |-  F/ y ps
3 rspc2v.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
4 rspc2v.2 . 2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
51, 2, 3, 4rspc2 2889 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:  rspc2va  2891  rspc3v  2893  disji2  4010  isorel  5823  isosolem  5844  fovcl  5949  caovclg  6012  caovcomg  6015  smoel  6377  fiint  7133  dffi3  7184  ltordlem  9298  seqhomo  11093  climcn2  12066  proplem  13592  drsdir  14069  latlem  14154  tsrlin  14328  laspwcl  14343  lanfwcl  14344  dirge  14359  mhmlin  14422  issubg2  14636  nsgbi  14648  ghmlin  14688  efgi  15028  efgred  15057  irredmul  15491  issubrg2  15565  abvmul  15594  abvtri  15595  lmodlema  15632  islmodd  15633  lmhmlin  15792  lbsind  15833  ipcj  16538  obsip  16621  inopn  16645  basis1  16688  basis2  16689  iscldtop  16832  hausnei  17056  t1sep2  17097  nconsubb  17149  r0sep  17439  fbasssin  17531  fcfneii  17732  xmeteq0  17903  nmvs  18187  cncfi  18398  c1lip1  19344  aalioulem3  19714  logltb  19953  cvxcl  20279  2sqlem8  20611  isgrp2d  20902  ablocom  20952  ghomlin  21031  ghgrplem2  21034  nvs  21228  nvtri  21236  phpar2  21401  phpar  21402  shaddcl  21796  shmulcl  21797  shmulclOLD  21798  cnopc  22493  unop  22495  hmop  22502  cnfnc  22510  adj1  22513  hstel2  22799  stj  22815  stcltr1i  22854  mddmdin0i  23011  cdj3lem1  23014  cdj3lem2b  23017  fovcld  23203  isoun  23242  disji2f  23354  disjif2  23358  pconcn  23755  ghomf1olem  24001  nocvxminlem  24344  nofulllem5  24360  brbtwn2  24533  axcontlem3  24594  axcontlem9  24600  axcontlem10  24601  labss1  25189  labss2  25191  oriso  25214  iscomb  25334  cmppfd  25745  domcmpd  25746  codcmpd  25747  cmpida  25774  cmpidb  25775  ismonb2  25812  cmpmon  25815  isepib2  25822  isibg2aa  26112  isibg2aalem1  26113  ivthALT  26258  ismtycnv  26526  ismtyima  26527  ismtyres  26532  bfplem1  26546  bfplem2  26547  rngohomadd  26600  rngohommul  26601  crngocom  26626  idladdcl  26644  idllmulcl  26645  idlrmulcl  26646  pridl  26662  ispridlc  26695  pridlc  26696  dmnnzd  26700  faovcl  28060  oposlem  29373  omllaw  29433  hlsuprexch  29570  lautle  30273  ltrnu  30310  tendovalco  30954
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