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

Theorem rspc2v 3072
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 3071 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 2709
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 2418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2714  df-v 2968
This theorem is referenced by:  rspc2va  3073  rspc3v  3075  disji2  4272  f1veqaeq  5965  isorel  6010  isosolem  6031  fovcl  6190  caovclg  6250  caovcomg  6253  smoel  6813  fiint  7580  dffi3  7673  ltordlem  9857  seqhomo  11845  climcn2  13062  proplem  14620  drsdir  15097  tsrlin  15381  dirge  15399  mhmlin  15463  issubg2  15685  nsgbi  15701  ghmlin  15741  efgi  16205  efgred  16234  irredmul  16787  issubrg2  16861  abvmul  16890  abvtri  16891  lmodlema  16929  islmodd  16930  lmhmlin  17090  lbsind  17135  ipcj  18032  obsip  18115  matecl  18295  inopn  18481  basis1  18524  basis2  18525  iscldtop  18668  hausnei  18901  t1sep2  18942  nconsubb  18996  r0sep  19290  fbasssin  19378  fcfneii  19579  ustssel  19749  xmeteq0  19882  nmvs  20226  cncfi  20439  c1lip1  21438  aalioulem3  21769  logltb  22017  cvxcl  22347  2sqlem8  22680  axtgcgrrflx  22892  axtgsegcon  22894  axtg5seg  22895  axtgbtwnid  22896  axtgpasch  22897  axtgcont1  22898  axtgupdim2  22901  axtgeucl  22902  f1otrgds  23060  f1otrg  23062  brbtwn2  23096  axcontlem3  23157  axcontlem9  23163  axcontlem10  23164  fargshiftf1  23468  isgrp2d  23667  ablocom  23717  ghomlin  23796  ghgrplem2  23799  nvs  23995  nvtri  24003  phpar2  24168  phpar  24169  shaddcl  24564  shmulcl  24565  shmulclOLD  24566  cnopc  25262  unop  25264  hmop  25271  cnfnc  25279  adj1  25282  hstel2  25568  stj  25584  stcltr1i  25623  mddmdin0i  25780  cdj3lem1  25783  cdj3lem2b  25786  disji2f  25866  disjif2  25870  disjxpin  25875  fovcld  25900  isoun  25942  tleile  26067  archirng  26150  archiexdiv  26152  slmdlema  26164  orngmul  26218  sibfof  26674  pconcn  27061  ghomf1olem  27260  nocvxminlem  27778  nofulllem5  27794  ivthALT  28473  ismtycnv  28644  ismtyima  28645  ismtyres  28650  bfplem1  28664  bfplem2  28665  rngohomadd  28718  rngohommul  28719  crngocom  28744  idladdcl  28762  idllmulcl  28763  idlrmulcl  28764  pridl  28780  ispridlc  28813  pridlc  28814  dmnnzd  28818  faovcl  30049  dmatelnd  30776  mdetdiaglem  30794  mdetdiagid  30796  oposlem  32578  omllaw  32639  hlsuprexch  32776  lautle  33479  ltrnu  33516  tendovalco  34160
  Copyright terms: Public domain W3C validator