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

Theorem rspc2v 3192
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 1752 . 2  |-  F/ x ch
2 nfv 1752 . 2  |-  F/ y ps
3 rspc2v.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
4 rspc2v.2 . 2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
51, 2, 3, 4rspc2 3191 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 188    /\ wa 371    = wceq 1438    e. wcel 1869   A.wral 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ral 2781  df-v 3084
This theorem is referenced by:  rspc2va  3193  rspc3v  3195  disji2  4408  f1veqaeq  6174  isorel  6230  isosolem  6251  oveqrspc2v  6326  fovcl  6413  caovclg  6473  caovcomg  6476  smoel  7085  fiint  7852  dffi3  7949  ltordlem  10141  seqhomo  12261  climcn2  13649  drsdir  16173  tsrlin  16458  dirge  16476  mhmlin  16582  issubg2  16825  nsgbi  16841  ghmlin  16881  efgi  17362  efgred  17391  irredmul  17930  issubrg2  18021  abvmul  18050  abvtri  18051  lmodlema  18089  islmodd  18090  lmhmlin  18251  lbsind  18296  mplcoe5lem  18684  ipcj  19193  obsip  19276  matecl  19442  dmatelnd  19513  scmateALT  19529  mdetdiaglem  19615  mdetdiagid  19617  pmatcoe1fsupp  19717  m2cpminvid2lem  19770  inopn  19921  basis1  19957  basis2  19958  iscldtop  20103  hausnei  20336  t1sep2  20377  nconsubb  20430  r0sep  20755  fbasssin  20843  fcfneii  21044  ustssel  21212  xmeteq0  21345  nmvs  21671  cncfi  21918  c1lip1  22941  aalioulem3  23282  logltb  23541  cvxcl  23902  2sqlem8  24292  axtgcgrrflx  24502  axtgsegcon  24504  axtg5seg  24505  axtgbtwnid  24506  axtgpasch  24507  axtgcont1  24508  axtgupdim2  24511  axtgeucl  24512  iscgrglt  24551  isperp2d  24753  f1otrgds  24891  brbtwn2  24927  axcontlem3  24988  axcontlem9  24994  axcontlem10  24995  fargshiftf1  25357  isgrp2d  25955  ablocom  26005  ghomlinOLD  26084  ghgrplem2OLD  26087  nvs  26283  nvtri  26291  phpar2  26456  phpar  26457  shaddcl  26862  shmulcl  26863  cnopc  27558  unop  27560  hmop  27567  cnfnc  27575  adj1  27578  hstel2  27864  stj  27880  stcltr1i  27919  mddmdin0i  28076  cdj3lem1  28079  cdj3lem2b  28082  disji2f  28183  disjif2  28187  disjxpin  28194  fovcld  28235  isoun  28278  archirng  28506  archiexdiv  28508  slmdlema  28520  inelcarsg  29145  sibfof  29175  axtgupdim2OLD  29487  pconcn  29949  ghomf1olem  30314  nocvxminlem  30578  nofulllem5  30594  ivthALT  30990  poimirlem32  31930  ismtycnv  32092  ismtyima  32093  ismtyres  32098  bfplem1  32112  bfplem2  32113  rngohomadd  32166  rngohommul  32167  crngocom  32192  idladdcl  32210  idllmulcl  32211  idlrmulcl  32212  pridl  32228  ispridlc  32261  pridlc  32262  dmnnzd  32266  oposlem  32711  omllaw  32772  hlsuprexch  32909  lautle  33612  ltrnu  33649  tendovalco  34295  mullimc  37560  mullimcf  37567  lptre2pt  37584  fourierdlem54  37888  faovcl  38458  icceuelpartlem  38505  iccpartnel  38508  mgmhmlin  39128  issubmgm2  39132
  Copyright terms: Public domain W3C validator