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

Theorem rspc2v 3223
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 1683 . 2  |-  F/ x ch
2 nfv 1683 . 2  |-  F/ y ps
3 rspc2v.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
4 rspc2v.2 . 2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
51, 2, 3, 4rspc2 3222 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 1379    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115
This theorem is referenced by:  rspc2va  3224  rspc3v  3226  disji2  4434  f1veqaeq  6157  isorel  6211  isosolem  6232  fovcl  6392  caovclg  6452  caovcomg  6455  smoel  7032  fiint  7798  dffi3  7892  ltordlem  10079  seqhomo  12123  climcn2  13381  proplem  14948  drsdir  15425  tsrlin  15709  dirge  15727  mhmlin  15796  issubg2  16030  nsgbi  16046  ghmlin  16086  efgi  16552  efgred  16581  irredmul  17171  issubrg2  17261  abvmul  17290  abvtri  17291  lmodlema  17329  islmodd  17330  lmhmlin  17493  lbsind  17538  ipcj  18476  obsip  18559  matecl  18734  dmatelnd  18805  scmateALT  18821  mdetdiaglem  18907  mdetdiagid  18909  pmatcoe1fsupp  19009  m2cpminvid2lem  19062  inopn  19215  basis1  19258  basis2  19259  iscldtop  19402  hausnei  19635  t1sep2  19676  nconsubb  19730  r0sep  20076  fbasssin  20164  fcfneii  20365  ustssel  20535  xmeteq0  20668  nmvs  21012  cncfi  21225  c1lip1  22225  aalioulem3  22556  logltb  22809  cvxcl  23139  2sqlem8  23472  axtgcgrrflx  23684  axtgsegcon  23686  axtg5seg  23687  axtgbtwnid  23688  axtgpasch  23689  axtgcont1  23690  axtgupdim2  23694  axtgeucl  23695  motcgr  23748  perpneq  23896  isperp2d  23898  foot  23901  f1otrgds  23945  f1otrg  23947  brbtwn2  23981  axcontlem3  24042  axcontlem9  24048  axcontlem10  24049  fargshiftf1  24410  isgrp2d  25010  ablocom  25060  ghomlin  25139  ghgrplem2  25142  nvs  25338  nvtri  25346  phpar2  25511  phpar  25512  shaddcl  25907  shmulcl  25908  shmulclOLD  25909  cnopc  26605  unop  26607  hmop  26614  cnfnc  26622  adj1  26625  hstel2  26911  stj  26927  stcltr1i  26966  mddmdin0i  27123  cdj3lem1  27126  cdj3lem2b  27129  disji2f  27208  disjif2  27212  disjxpin  27217  fovcld  27248  isoun  27289  tleile  27408  archirng  27491  archiexdiv  27493  slmdlema  27505  orngmul  27553  sibfof  28033  pconcn  28420  ghomf1olem  28785  nocvxminlem  29303  nofulllem5  29319  ivthALT  30006  ismtycnv  30128  ismtyima  30129  ismtyres  30134  bfplem1  30148  bfplem2  30149  rngohomadd  30202  rngohommul  30203  crngocom  30228  idladdcl  30246  idllmulcl  30247  idlrmulcl  30248  pridl  30264  ispridlc  30297  pridlc  30298  dmnnzd  30302  mullimc  31385  mullimcf  31392  lptre2pt  31409  fourierdlem54  31688  faovcl  31979  oposlem  34196  omllaw  34257  hlsuprexch  34394  lautle  35097  ltrnu  35134  tendovalco  35778
  Copyright terms: Public domain W3C validator