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

Theorem rspc2v 3203
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 1692 . 2  |-  F/ x ch
2 nfv 1692 . 2  |-  F/ y ps
3 rspc2v.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
4 rspc2v.2 . 2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
51, 2, 3, 4rspc2 3202 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 1381    e. wcel 1802   A.wral 2791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-v 3095
This theorem is referenced by:  rspc2va  3204  rspc3v  3206  disji2  4421  f1veqaeq  6150  isorel  6204  isosolem  6225  oveqrspc2v  6301  fovcl  6389  caovclg  6449  caovcomg  6452  smoel  7030  fiint  7796  dffi3  7890  ltordlem  10081  seqhomo  12130  climcn2  13391  drsdir  15435  tsrlin  15720  dirge  15738  mhmlin  15844  issubg2  16087  nsgbi  16103  ghmlin  16143  efgi  16608  efgred  16637  irredmul  17229  issubrg2  17320  abvmul  17349  abvtri  17350  lmodlema  17388  islmodd  17389  lmhmlin  17552  lbsind  17597  mplcoe5lem  18001  ipcj  18539  obsip  18622  matecl  18797  dmatelnd  18868  scmateALT  18884  mdetdiaglem  18970  mdetdiagid  18972  pmatcoe1fsupp  19072  m2cpminvid2lem  19125  inopn  19278  basis1  19321  basis2  19322  iscldtop  19466  hausnei  19699  t1sep2  19740  nconsubb  19794  r0sep  20119  fbasssin  20207  fcfneii  20408  ustssel  20578  xmeteq0  20711  nmvs  21055  cncfi  21268  c1lip1  22268  aalioulem3  22599  logltb  22853  cvxcl  23183  2sqlem8  23516  axtgcgrrflx  23728  axtgsegcon  23730  axtg5seg  23731  axtgbtwnid  23732  axtgpasch  23733  axtgcont1  23734  axtgupdim2  23738  axtgeucl  23739  isperp2d  23962  f1otrgds  24041  brbtwn2  24077  axcontlem3  24138  axcontlem9  24144  axcontlem10  24145  fargshiftf1  24506  isgrp2d  25106  ablocom  25156  ghomlinOLD  25235  ghgrplem2OLD  25238  nvs  25434  nvtri  25442  phpar2  25607  phpar  25608  shaddcl  26003  shmulcl  26004  shmulclOLD  26005  cnopc  26701  unop  26703  hmop  26710  cnfnc  26718  adj1  26721  hstel2  27007  stj  27023  stcltr1i  27062  mddmdin0i  27219  cdj3lem1  27222  cdj3lem2b  27225  disji2f  27307  disjif2  27311  disjxpin  27316  fovcld  27347  isoun  27389  archirng  27602  archiexdiv  27604  slmdlema  27616  sibfof  28152  pconcn  28539  ghomf1olem  28904  nocvxminlem  29422  nofulllem5  29438  ivthALT  30125  ismtycnv  30270  ismtyima  30271  ismtyres  30276  bfplem1  30290  bfplem2  30291  rngohomadd  30344  rngohommul  30345  crngocom  30370  idladdcl  30388  idllmulcl  30389  idlrmulcl  30390  pridl  30406  ispridlc  30439  pridlc  30440  dmnnzd  30444  mullimc  31530  mullimcf  31537  lptre2pt  31554  fourierdlem54  31832  faovcl  32123  mgmhmlin  32312  issubmgm2  32316  oposlem  34630  omllaw  34691  hlsuprexch  34828  lautle  35531  ltrnu  35568  tendovalco  36214
  Copyright terms: Public domain W3C validator