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

Theorem cbvralv 2968
Description: Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)
Hypothesis
Ref Expression
cbvralv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvralv  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Distinct variable groups:    x, A    y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvralv
StepHypRef Expression
1 nfv 1673 . 2  |-  F/ y
ph
2 nfv 1673 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2964 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   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-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2741
This theorem is referenced by:  cbvral2v  2976  cbvral3v  2978  reu7  3175  disjxun  4311  reusv3i  4520  wereu2  4738  cnvpo  5396  f1mpt  5995  grprinvlem  6322  grprinvd  6323  dfwe2  6414  tfinds  6491  tfrlem1  6856  tfrlem12  6869  rdglem1  6892  tz7.48lem  6917  nneneq  7515  marypha1lem  7704  supub  7730  suplub  7731  supmaxlem  7735  ordtypecbv  7752  ordtypelem3  7755  ordtypelem9  7761  wemaplem1  7781  brwdom3  7818  tcrank  8112  infxpenc2  8209  infxpenc2OLD  8213  aceq1  8308  aceq2  8310  dfac5  8319  dfac9  8326  dfac12lem3  8335  kmlem12  8351  kmlem14  8353  cofsmo  8459  infpssrlem4  8496  isfin3ds  8519  isf32lem2  8544  isf32lem11  8553  isf33lem  8556  domtriomlem  8632  axdc3  8644  zorn2lem7  8692  zorn2g  8693  fpwwe2cbv  8818  fpwwecbv  8832  pwfseq  8852  axgroth6  9016  dedekind  9554  suprleub  10315  infmrgelb  10331  nnsub  10381  uzwo  10938  uzwoOLD  10939  ublbneg  10960  zsupss  10965  xrub  11295  monoord2  11858  faclbnd4lem4  12093  bccl  12119  hashbc  12227  wrdind  12392  wrd2ind  12393  cau3lem  12863  climmpt2  13072  caucvgrlem  13171  caurcvg2  13176  caucvgb  13178  fsum0diag2  13271  incexclem  13320  cvgrat  13364  mertenslem2  13366  mertens  13367  sqr2irr  13552  gcdcllem1  13716  prmind2  13795  prmpwdvds  13986  prmreclem5  14002  prmreclem6  14003  vdwlem7  14069  vdwlem10  14072  vdwlem13  14075  vdwnn  14080  ramcl  14111  isacs2  14612  catpropd  14669  mrcmndind  15515  gsumvalx  15523  issubg4  15721  isnsg2  15732  elnmz  15741  gsmsymgreqlem2  15957  psgnunilem5  16021  psgnunilem3  16023  efgsdm  16248  pgpfac1lem5  16602  pgpfac1  16603  pgpfac  16607  ablfaclem3  16610  lbsextg  17265  evlslem2  17619  mpfind  17644  mdetuni0  18449  elcls3  18709  isclo2  18714  neiptopnei  18758  tgcn  18878  subbascn  18880  txcmplem2  19237  kqfvima  19325  kqt0lem  19331  isr0  19332  r0cld  19333  regr1lem2  19335  fbun  19435  flftg  19591  fclsbas  19616  alexsubALTlem2  19642  alexsubALTlem4  19644  ptcmplem4  19649  tsmsxplem1  19749  tsmsxp  19751  ustuqtop  19843  utopsnneip  19845  prdsxmslem2  20126  iscau4  20812  caucfil  20816  iscmet3  20826  bcthlem5  20861  bcth  20862  ovolicc2lem5  21026  uniioombllem6  21090  vitali  21115  ismbf3d  21154  itg1climres  21214  itg2seq  21242  itg2monolem1  21250  itg2mono  21253  rolle  21484  dvlipcn  21488  dvivthlem1  21502  ply1divex  21630  fta1g  21661  dgrco  21764  plydivex  21785  fta1  21796  vieta1  21800  ulmcaulem  21881  ulmcau  21882  abelthlem8  21926  wilth  22431  fta  22439  dchrelbas3  22599  2sqlem6  22730  2sqlem10  22735  dchrisumlem3  22762  dchrisum  22763  dchrmusumlema  22764  dchrvmasumlema  22771  dchrisum0lema  22785  pntibndlem3  22863  pntlem3  22880  pntleml  22882  pnt3  22883  ostth2lem2  22905  ostth  22910  axcontlem1  23232  axcontlem6  23237  cusgrafilem2  23410  grpoideu  23718  ubthlem3  24295  adjsym  25259  lnopunilem1  25436  elunop2  25439  lnophm  25445  cnlnadjlem5  25497  mdbr3  25723  mdbr4  25724  dmdbr3  25731  dmdbr4  25732  mddmd2  25735  toslublem  26150  tosglblem  26152  archiabl  26237  isarchiofld  26307  lmdvg  26405  esumcvg  26557  eulerpartlemsv3  26766  eulerpartlemgvv  26781  signstfvneq0  26995  derangenlem  27081  subfacp1lem6  27095  subfacp1  27096  rescon  27157  cvmscbv  27169  untangtr  27387  dfon2lem3  27620  dfon2lem7  27624  cbvsetlike  27664  wfrlem1  27746  frrlem1  27790  heicant  28452  mblfinlem2  28455  ovoliunnfl  28459  voliunnfl  28461  mbfresfi  28464  nn0prpwlem  28543  neibastop3  28609  fnemeet2  28614  upixp  28649  sdclem2  28664  fdc  28667  mettrifi  28679  heiborlem5  28740  heiborlem10  28745  heibor  28746  bfp  28749  mzpclval  29087  dford3lem1  29401  fnwe2lem1  29429  aomclem3  29435  aomclem4  29436  aomclem8  29440  dfac11  29441  hbtlem5  29510  fnchoice  29777  cncmpmax  29780  climsuse  29807  stoweidlem7  29828  stoweidlem15  29836  stoweidlem35  29856  wallispilem3  29888  reuccats1  30287  usg2wlkeq  30315  fsuppmapnn0fiubex  30830  gsummptnn0fzfv  30841  cply1mul  30884  m2pminv2lem  31100  mp2pm2mplem4  31134  bnj1185  31883  bnj1379  31920  bnj222  31972  bnj517  31974  bnj1450  32137  bnj1452  32139  bnj1463  32142  cdleme25cv  34098  cdleme40v  34209
  Copyright terms: Public domain W3C validator