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

Theorem rspc2v 2924
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 1610 . 2  |-  F/ x ch
2 nfv 1610 . 2  |-  F/ y ps
3 rspc2v.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
4 rspc2v.2 . 2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
51, 2, 3, 4rspc2 2923 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A. x  e.  C  A. y  e.  D  ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1633    e. wcel 1701   A.wral 2577
This theorem is referenced by:  rspc2va  2925  rspc3v  2927  disji2  4047  isorel  5865  isosolem  5886  fovcl  5991  caovclg  6054  caovcomg  6057  smoel  6419  fiint  7178  dffi3  7229  ltordlem  9343  seqhomo  11140  climcn2  12113  proplem  13641  drsdir  14118  latlem  14203  tsrlin  14377  laspwcl  14392  lanfwcl  14393  dirge  14408  mhmlin  14471  issubg2  14685  nsgbi  14697  ghmlin  14737  efgi  15077  efgred  15106  irredmul  15540  issubrg2  15614  abvmul  15643  abvtri  15644  lmodlema  15681  islmodd  15682  lmhmlin  15841  lbsind  15882  ipcj  16594  obsip  16677  inopn  16701  basis1  16744  basis2  16745  iscldtop  16888  hausnei  17112  t1sep2  17153  nconsubb  17205  r0sep  17495  fbasssin  17583  fcfneii  17784  xmeteq0  17955  nmvs  18239  cncfi  18450  c1lip1  19397  aalioulem3  19767  logltb  20006  cvxcl  20332  2sqlem8  20664  isgrp2d  20955  ablocom  21005  ghomlin  21084  ghgrplem2  21087  nvs  21283  nvtri  21291  phpar2  21456  phpar  21457  shaddcl  21851  shmulcl  21852  shmulclOLD  21853  cnopc  22548  unop  22550  hmop  22557  cnfnc  22565  adj1  22568  hstel2  22854  stj  22870  stcltr1i  22909  mddmdin0i  23066  cdj3lem1  23069  cdj3lem2b  23072  disji2f  23162  disjif2  23166  fovcld  23200  isoun  23239  ustssel  23422  pconcn  24039  ghomf1olem  24285  nocvxminlem  24729  nofulllem5  24745  brbtwn2  24919  axcontlem3  24980  axcontlem9  24986  axcontlem10  24987  ivthALT  25407  ismtycnv  25674  ismtyima  25675  ismtyres  25680  bfplem1  25694  bfplem2  25695  rngohomadd  25748  rngohommul  25749  crngocom  25774  idladdcl  25792  idllmulcl  25793  idlrmulcl  25794  pridl  25810  ispridlc  25843  pridlc  25844  dmnnzd  25848  faovcl  27213  f1veqaeq  27242  fargshiftf1  27520  oposlem  29191  omllaw  29251  hlsuprexch  29388  lautle  30091  ltrnu  30128  tendovalco  30772
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-v 2824
  Copyright terms: Public domain W3C validator