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

Theorem cbvralv 3053
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 1751 . 2  |-  F/ y
ph
2 nfv 1751 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 3049 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wral 2773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-sb 1787  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ral 2778
This theorem is referenced by:  cbvral2v  3061  cbvral3v  3063  reu7  3263  disjxun  4415  reusv3i  4624  wereu2  4843  cnvpo  5386  f1mpt  6169  grprinvlem  6513  grprinvd  6514  dfwe2  6614  tfinds  6692  wfrlem1  7035  tfrlem1  7094  tfrlem12  7107  rdglem1  7133  tz7.48lem  7158  nneneq  7753  marypha1lem  7945  supub  7971  suplub  7972  supmaxlemOLD  7980  ordtypecbv  8030  ordtypelem3  8033  ordtypelem9  8039  wemaplem1  8059  brwdom3  8095  tcrank  8352  infxpenc2  8449  aceq1  8544  aceq2  8546  dfac5  8555  dfac9  8562  dfac12lem3  8571  kmlem12  8587  kmlem14  8589  cofsmo  8695  infpssrlem4  8732  isfin3ds  8755  isf32lem2  8780  isf32lem11  8789  isf33lem  8792  domtriomlem  8868  axdc3  8880  zorn2lem7  8928  zorn2g  8929  fpwwe2cbv  9051  fpwwecbv  9065  pwfseq  9085  axgroth6  9249  dedekind  9793  suprleub  10569  infregelb  10590  infmrgelbOLD  10591  nnsub  10644  uzwo  11218  ublbneg  11244  zsupss  11249  xrub  11593  fsuppmapnn0fiubex  12197  monoord2  12237  faclbnd4lem4  12474  bccl  12500  hashbc  12607  wrdind  12814  wrd2ind  12815  reuccats1  12818  cau3lem  13396  climmpt2  13615  caucvgrlem  13714  caucvgrlemOLD  13715  caurcvg2  13722  caucvgb  13724  fsum0diag2  13822  incexclem  13872  cvgrat  13917  mertenslem2  13919  mertens  13920  sqrt2irr  14279  gcdcllem1  14451  lcmfunsnlem1  14588  lcmfunsnlem2lem1  14589  prmind2  14613  prmpwdvds  14826  prmreclem5  14842  prmreclem6  14843  vdwlem7  14915  vdwlem10  14918  vdwlem13  14921  vdwnn  14926  ramcl  14965  prmgaplcmlem1OLD  14990  prmordvdslcmsOLDOLD  14999  isacs2  15537  catpropd  15592  gsumvalx  16491  mrcmndind  16591  issubg4  16814  isnsg2  16825  elnmz  16834  gsmsymgreqlem2  17050  psgnunilem5  17113  psgnunilem3  17115  efgsdm  17358  gsummptnn0fzfv  17595  pgpfac1lem5  17690  pgpfac1  17691  pgpfac  17695  ablfaclem3  17698  lbsextg  18363  evlslem2  18713  mpfind  18737  cply1mul  18865  mdetuni0  19623  m2cpminvid2lem  19755  mp2pm2mplem4  19810  chcoeffeqlem  19886  cayhamlem3  19888  elcls3  20076  isclo2  20081  neiptopnei  20125  tgcn  20245  subbascn  20247  txcmplem2  20634  kqfvima  20722  kqt0lem  20728  isr0  20729  r0cld  20730  regr1lem2  20732  fbun  20832  flftg  20988  fclsbas  21013  alexsubALTlem2  21040  alexsubALTlem4  21042  ptcmplem4  21047  tsmsxplem1  21144  tsmsxp  21146  ustuqtop  21238  utopsnneip  21240  prdsxmslem2  21521  iscau4  22226  caucfil  22230  iscmet3  22240  bcthlem5  22273  bcth  22274  ovolicc2lem5  22452  uniioombllem6  22523  vitali  22548  ismbf3d  22587  itg1climres  22649  itg2seq  22677  itg2monolem1  22685  itg2mono  22688  rolle  22919  dvlipcn  22923  dvivthlem1  22937  ply1divex  23064  fta1g  23095  dgrco  23206  plydivex  23227  fta1  23238  vieta1  23242  ulmcaulem  23326  ulmcau  23327  abelthlem8  23371  wilth  23973  fta  23983  dchrelbas3  24143  2sqlem6  24274  2sqlem10  24279  dchrisumlem3  24306  dchrisum  24307  dchrmusumlema  24308  dchrvmasumlema  24315  dchrisum0lema  24329  pntibndlem3  24407  pntlem3  24424  pntleml  24426  pnt3  24427  ostth2lem2  24449  ostth  24454  axcontlem1  24971  axcontlem6  24976  cusgrafilem2  25184  usg2wlkeq  25412  grpoideu  25913  ubthlem3  26490  adjsym  27462  lnopunilem1  27639  elunop2  27642  lnophm  27648  cnlnadjlem5  27700  mdbr3  27926  mdbr4  27927  dmdbr3  27934  dmdbr4  27935  mddmd2  27938  toslublem  28415  tosglblem  28417  archiabl  28503  isarchiofld  28569  qtophaus  28652  lmdvg  28748  esumcvg  28896  unelldsys  28969  ldgenpisyslem1  28974  eulerpartlemsv3  29183  eulerpartlemgvv  29198  signstfvneq0  29450  bnj1185  29594  bnj1379  29631  bnj222  29683  bnj517  29685  bnj1450  29848  bnj1452  29850  bnj1463  29853  derangenlem  29883  subfacp1lem6  29897  subfacp1  29898  rescon  29958  cvmscbv  29970  untangtr  30330  dfon2lem3  30419  dfon2lem7  30423  frrlem1  30502  nn0prpwlem  30964  neibastop3  31004  fnemeet2  31009  phpreu  31837  poimirlem27  31875  heicant  31883  mblfinlem2  31886  ovoliunnfl  31890  voliunnfl  31892  mbfresfi  31895  upixp  31964  sdclem2  31979  fdc  31982  mettrifi  31994  heiborlem5  32055  heiborlem10  32060  heibor  32061  bfp  32064  cdleme25cv  33838  cdleme40v  33949  mzpclval  35480  dford3lem1  35795  fnwe2lem1  35822  aomclem3  35828  aomclem4  35829  aomclem8  35833  dfac11  35834  hbtlem5  35901  fnchoice  37205  cncmpmax  37208  wessf1ornlem  37297  disjinfi  37306  mccl  37465  climsuse  37474  limsupre  37508  limsupreOLD  37509  dvbdfbdioolem2  37588  dvbdfbdioo  37589  ioodvbdlimc1lem1  37590  ioodvbdlimc1lem2  37591  ioodvbdlimc1lem1OLD  37592  ioodvbdlimc1lem2OLD  37593  ioodvbdlimc2lem  37595  ioodvbdlimc2lemOLD  37596  dvnprodlem3  37610  stoweidlem7  37654  stoweidlem15  37662  stoweidlem35  37683  wallispilem3  37716  fourierdlem68  37825  fourierdlem71  37828  fourierdlem73  37830  fourierdlem87  37844  fourierdlem100  37857  fourierdlem103  37860  fourierdlem104  37861  fourierdlem107  37864  fourierdlem109  37866  fourierdlem112  37869  etransc  37936  bgoldbtbndlem4  38523  bgoldbtbnd  38524  nn0sumshdiglem1  39497
  Copyright terms: Public domain W3C validator