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

Theorem rspc2v 3157
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 1722 . 2  |-  F/ x ch
2 nfv 1722 . 2  |-  F/ y ps
3 rspc2v.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
4 rspc2v.2 . 2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
51, 2, 3, 4rspc2 3156 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 1399    e. wcel 1836   A.wral 2742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ral 2747  df-v 3049
This theorem is referenced by:  rspc2va  3158  rspc3v  3160  disji2  4367  f1veqaeq  6085  isorel  6141  isosolem  6162  oveqrspc2v  6237  fovcl  6324  caovclg  6384  caovcomg  6387  smoel  6967  fiint  7730  dffi3  7824  ltordlem  10013  seqhomo  12076  climcn2  13436  drsdir  15700  tsrlin  15985  dirge  16003  mhmlin  16109  issubg2  16352  nsgbi  16368  ghmlin  16408  efgi  16873  efgred  16902  irredmul  17490  issubrg2  17581  abvmul  17610  abvtri  17611  lmodlema  17649  islmodd  17650  lmhmlin  17813  lbsind  17858  mplcoe5lem  18262  ipcj  18779  obsip  18862  matecl  19031  dmatelnd  19102  scmateALT  19118  mdetdiaglem  19204  mdetdiagid  19206  pmatcoe1fsupp  19306  m2cpminvid2lem  19359  inopn  19512  basis1  19555  basis2  19556  iscldtop  19701  hausnei  19934  t1sep2  19975  nconsubb  20028  r0sep  20353  fbasssin  20441  fcfneii  20642  ustssel  20812  xmeteq0  20945  nmvs  21289  cncfi  21502  c1lip1  22502  aalioulem3  22834  logltb  23091  cvxcl  23450  2sqlem8  23783  axtgcgrrflx  23996  axtgsegcon  23998  axtg5seg  23999  axtgbtwnid  24000  axtgpasch  24001  axtgcont1  24002  axtgupdim2OLD  24006  axtgupdim2  24007  axtgeucl  24008  isperp2d  24234  f1otrgds  24314  brbtwn2  24350  axcontlem3  24411  axcontlem9  24417  axcontlem10  24418  fargshiftf1  24779  isgrp2d  25375  ablocom  25425  ghomlinOLD  25504  ghgrplem2OLD  25507  nvs  25703  nvtri  25711  phpar2  25876  phpar  25877  shaddcl  26272  shmulcl  26273  shmulclOLD  26274  cnopc  26969  unop  26971  hmop  26978  cnfnc  26986  adj1  26989  hstel2  27275  stj  27291  stcltr1i  27330  mddmdin0i  27487  cdj3lem1  27490  cdj3lem2b  27493  disji2f  27596  disjif2  27600  disjxpin  27607  fovcld  27648  isoun  27697  archirng  27915  archiexdiv  27917  slmdlema  27929  inelcarsg  28474  sibfof  28501  pconcn  28894  ghomf1olem  29259  nocvxminlem  29651  nofulllem5  29667  ivthALT  30355  ismtycnv  30500  ismtyima  30501  ismtyres  30506  bfplem1  30520  bfplem2  30521  rngohomadd  30574  rngohommul  30575  crngocom  30600  idladdcl  30618  idllmulcl  30619  idlrmulcl  30620  pridl  30636  ispridlc  30669  pridlc  30670  dmnnzd  30674  mullimc  31823  mullimcf  31830  lptre2pt  31847  fourierdlem54  32144  faovcl  32486  mgmhmlin  32827  issubmgm2  32831  oposlem  35355  omllaw  35416  hlsuprexch  35553  lautle  36256  ltrnu  36293  tendovalco  36939
  Copyright terms: Public domain W3C validator