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

Theorem rspc2v 3059
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 1630 . 2  |-  F/ x ch
2 nfv 1630 . 2  |-  F/ y ps
3 rspc2v.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
4 rspc2v.2 . 2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
51, 2, 3, 4rspc2 3058 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 178    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2706
This theorem is referenced by:  rspc2va  3060  rspc3v  3062  disji2  4200  f1veqaeq  6006  isorel  6047  isosolem  6068  fovcl  6176  caovclg  6240  caovcomg  6243  smoel  6623  fiint  7384  dffi3  7437  ltordlem  9553  seqhomo  11371  climcn2  12387  proplem  13916  drsdir  14393  latlem  14478  tsrlin  14652  laspwcl  14667  lanfwcl  14668  dirge  14683  mhmlin  14746  issubg2  14960  nsgbi  14972  ghmlin  15012  efgi  15352  efgred  15381  irredmul  15815  issubrg2  15889  abvmul  15918  abvtri  15919  lmodlema  15956  islmodd  15957  lmhmlin  16112  lbsind  16153  ipcj  16866  obsip  16949  inopn  16973  basis1  17016  basis2  17017  iscldtop  17160  hausnei  17393  t1sep2  17434  nconsubb  17487  r0sep  17781  fbasssin  17869  fcfneii  18070  ustssel  18236  xmeteq0  18369  nmvs  18713  cncfi  18925  c1lip1  19882  aalioulem3  20252  logltb  20495  cvxcl  20824  2sqlem8  21157  fargshiftf1  21625  isgrp2d  21824  ablocom  21874  ghomlin  21953  ghgrplem2  21956  nvs  22152  nvtri  22160  phpar2  22325  phpar  22326  shaddcl  22720  shmulcl  22721  shmulclOLD  22722  cnopc  23417  unop  23419  hmop  23426  cnfnc  23434  adj1  23437  hstel2  23723  stj  23739  stcltr1i  23778  mddmdin0i  23935  cdj3lem1  23938  cdj3lem2b  23941  disji2f  24020  disjif2  24024  disjxpin  24029  fovcld  24051  isoun  24090  tleile  24190  sibfof  24655  pconcn  24912  ghomf1olem  25106  nocvxminlem  25646  nofulllem5  25662  brbtwn2  25845  axcontlem3  25906  axcontlem9  25912  axcontlem10  25913  ivthALT  26339  ismtycnv  26512  ismtyima  26513  ismtyres  26518  bfplem1  26532  bfplem2  26533  rngohomadd  26586  rngohommul  26587  crngocom  26612  idladdcl  26630  idllmulcl  26631  idlrmulcl  26632  pridl  26648  ispridlc  26681  pridlc  26682  dmnnzd  26686  faovcl  28041  oposlem  29982  omllaw  30042  hlsuprexch  30179  lautle  30882  ltrnu  30919  tendovalco  31563
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-v 2959
  Copyright terms: Public domain W3C validator