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

Theorem rspc2v 3100
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 1673 . 2  |-  F/ x ch
2 nfv 1673 . 2  |-  F/ y ps
3 rspc2v.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
4 rspc2v.2 . 2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
51, 2, 3, 4rspc2 3099 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 1369    e. wcel 1756   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2741  df-v 2995
This theorem is referenced by:  rspc2va  3101  rspc3v  3103  disji2  4300  f1veqaeq  5993  isorel  6038  isosolem  6059  fovcl  6216  caovclg  6276  caovcomg  6279  smoel  6842  fiint  7609  dffi3  7702  ltordlem  9886  seqhomo  11874  climcn2  13091  proplem  14649  drsdir  15126  tsrlin  15410  dirge  15428  mhmlin  15492  issubg2  15717  nsgbi  15733  ghmlin  15773  efgi  16237  efgred  16266  irredmul  16823  issubrg2  16907  abvmul  16936  abvtri  16937  lmodlema  16975  islmodd  16976  lmhmlin  17138  lbsind  17183  ipcj  18085  obsip  18168  matecl  18348  inopn  18534  basis1  18577  basis2  18578  iscldtop  18721  hausnei  18954  t1sep2  18995  nconsubb  19049  r0sep  19343  fbasssin  19431  fcfneii  19632  ustssel  19802  xmeteq0  19935  nmvs  20279  cncfi  20492  c1lip1  21491  aalioulem3  21822  logltb  22070  cvxcl  22400  2sqlem8  22733  axtgcgrrflx  22945  axtgsegcon  22947  axtg5seg  22948  axtgbtwnid  22949  axtgpasch  22950  axtgcont1  22951  axtgupdim2  22954  axtgeucl  22955  perpneq  23127  isperp2d  23129  foot  23132  f1otrgds  23137  f1otrg  23139  brbtwn2  23173  axcontlem3  23234  axcontlem9  23240  axcontlem10  23241  fargshiftf1  23545  isgrp2d  23744  ablocom  23794  ghomlin  23873  ghgrplem2  23876  nvs  24072  nvtri  24080  phpar2  24245  phpar  24246  shaddcl  24641  shmulcl  24642  shmulclOLD  24643  cnopc  25339  unop  25341  hmop  25348  cnfnc  25356  adj1  25359  hstel2  25645  stj  25661  stcltr1i  25700  mddmdin0i  25857  cdj3lem1  25860  cdj3lem2b  25863  disji2f  25943  disjif2  25947  disjxpin  25952  fovcld  25977  isoun  26019  tleile  26144  archirng  26227  archiexdiv  26229  slmdlema  26241  orngmul  26293  sibfof  26748  pconcn  27135  ghomf1olem  27335  nocvxminlem  27853  nofulllem5  27869  ivthALT  28556  ismtycnv  28727  ismtyima  28728  ismtyres  28733  bfplem1  28747  bfplem2  28748  rngohomadd  28801  rngohommul  28802  crngocom  28827  idladdcl  28845  idllmulcl  28846  idlrmulcl  28847  pridl  28863  ispridlc  28896  pridlc  28897  dmnnzd  28901  faovcl  30132  dmatelnd  30914  mdetdiaglem  30932  mdetdiagid  30934  pmatcoe1fsupp  31107  oposlem  32923  omllaw  32984  hlsuprexch  33121  lautle  33824  ltrnu  33861  tendovalco  34505
  Copyright terms: Public domain W3C validator