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

Theorem cbvralv 3088
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 1683 . 2  |-  F/ y
ph
2 nfv 1683 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 3084 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 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-or 370  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819
This theorem is referenced by:  cbvral2v  3096  cbvral3v  3098  reu7  3298  disjxun  4445  reusv3i  4654  wereu2  4876  cnvpo  5545  f1mpt  6157  grprinvlem  6497  grprinvd  6498  dfwe2  6601  tfinds  6678  tfrlem1  7045  tfrlem12  7058  rdglem1  7081  tz7.48lem  7106  nneneq  7700  marypha1lem  7893  supub  7919  suplub  7920  supmaxlem  7924  ordtypecbv  7942  ordtypelem3  7945  ordtypelem9  7951  wemaplem1  7971  brwdom3  8008  tcrank  8302  infxpenc2  8399  infxpenc2OLD  8403  aceq1  8498  aceq2  8500  dfac5  8509  dfac9  8516  dfac12lem3  8525  kmlem12  8541  kmlem14  8543  cofsmo  8649  infpssrlem4  8686  isfin3ds  8709  isf32lem2  8734  isf32lem11  8743  isf33lem  8746  domtriomlem  8822  axdc3  8834  zorn2lem7  8882  zorn2g  8883  fpwwe2cbv  9008  fpwwecbv  9022  pwfseq  9042  axgroth6  9206  dedekind  9743  suprleub  10507  infmrgelb  10523  nnsub  10574  uzwo  11144  uzwoOLD  11145  ublbneg  11166  zsupss  11171  xrub  11503  fsuppmapnn0fiubex  12066  monoord2  12106  faclbnd4lem4  12342  bccl  12368  hashbc  12468  wrdind  12665  wrd2ind  12666  reuccats1  12669  cau3lem  13150  climmpt2  13359  caucvgrlem  13458  caurcvg2  13463  caucvgb  13465  fsum0diag2  13561  incexclem  13611  cvgrat  13655  mertenslem2  13657  mertens  13658  sqrt2irr  13843  gcdcllem1  14008  prmind2  14087  prmpwdvds  14281  prmreclem5  14297  prmreclem6  14298  vdwlem7  14364  vdwlem10  14367  vdwlem13  14370  vdwnn  14375  ramcl  14406  isacs2  14908  catpropd  14965  mrcmndind  15816  gsumvalx  15824  issubg4  16025  isnsg2  16036  elnmz  16045  gsmsymgreqlem2  16261  psgnunilem5  16325  psgnunilem3  16327  efgsdm  16554  gsummptnn0fzfv  16819  pgpfac1lem5  16932  pgpfac1  16933  pgpfac  16937  ablfaclem3  16940  lbsextg  17608  evlslem2  17979  mpfind  18004  cply1mul  18134  mdetuni0  18918  m2cpminvid2lem  19050  mp2pm2mplem4  19105  chcoeffeqlem  19181  cayhamlem3  19183  elcls3  19378  isclo2  19383  neiptopnei  19427  tgcn  19547  subbascn  19549  txcmplem2  19906  kqfvima  19994  kqt0lem  20000  isr0  20001  r0cld  20002  regr1lem2  20004  fbun  20104  flftg  20260  fclsbas  20285  alexsubALTlem2  20311  alexsubALTlem4  20313  ptcmplem4  20318  tsmsxplem1  20418  tsmsxp  20420  ustuqtop  20512  utopsnneip  20514  prdsxmslem2  20795  iscau4  21481  caucfil  21485  iscmet3  21495  bcthlem5  21530  bcth  21531  ovolicc2lem5  21695  uniioombllem6  21760  vitali  21785  ismbf3d  21824  itg1climres  21884  itg2seq  21912  itg2monolem1  21920  itg2mono  21923  rolle  22154  dvlipcn  22158  dvivthlem1  22172  ply1divex  22300  fta1g  22331  dgrco  22434  plydivex  22455  fta1  22466  vieta1  22470  ulmcaulem  22551  ulmcau  22552  abelthlem8  22596  wilth  23101  fta  23109  dchrelbas3  23269  2sqlem6  23400  2sqlem10  23405  dchrisumlem3  23432  dchrisum  23433  dchrmusumlema  23434  dchrvmasumlema  23441  dchrisum0lema  23455  pntibndlem3  23533  pntlem3  23550  pntleml  23552  pnt3  23553  ostth2lem2  23575  ostth  23580  axcontlem1  23971  axcontlem6  23976  cusgrafilem2  24184  usg2wlkeq  24412  grpoideu  24915  ubthlem3  25492  adjsym  26456  lnopunilem1  26633  elunop2  26636  lnophm  26642  cnlnadjlem5  26694  mdbr3  26920  mdbr4  26921  dmdbr3  26928  dmdbr4  26929  mddmd2  26932  toslublem  27345  tosglblem  27347  archiabl  27432  isarchiofld  27498  lmdvg  27599  qtophaus  27665  esumcvg  27760  eulerpartlemsv3  27968  eulerpartlemgvv  27983  signstfvneq0  28197  derangenlem  28283  subfacp1lem6  28297  subfacp1  28298  rescon  28359  cvmscbv  28371  untangtr  28589  dfon2lem3  28822  dfon2lem7  28826  cbvsetlike  28866  wfrlem1  28948  frrlem1  28992  heicant  29654  mblfinlem2  29657  ovoliunnfl  29661  voliunnfl  29663  mbfresfi  29666  nn0prpwlem  29745  neibastop3  29811  fnemeet2  29816  upixp  29851  sdclem2  29866  fdc  29869  mettrifi  29881  heiborlem5  29942  heiborlem10  29947  heibor  29948  bfp  29951  mzpclval  30289  dford3lem1  30600  fnwe2lem1  30628  aomclem3  30634  aomclem4  30635  aomclem8  30639  dfac11  30640  hbtlem5  30709  fnchoice  31010  cncmpmax  31013  climsuse  31178  limsupre  31211  dvbdfbdioolem2  31287  dvbdfbdioo  31288  ioodvbdlimc1lem1  31289  ioodvbdlimc1lem2  31290  ioodvbdlimc2lem  31292  stoweidlem7  31335  stoweidlem15  31343  stoweidlem35  31363  wallispilem3  31395  fourierdlem45  31480  fourierdlem71  31506  fourierdlem73  31508  fourierdlem87  31522  fourierdlem100  31535  fourierdlem103  31538  fourierdlem104  31539  fourierdlem107  31542  fourierdlem109  31544  fourierdlem112  31547  bnj1185  32949  bnj1379  32986  bnj222  33038  bnj517  33040  bnj1450  33203  bnj1452  33205  bnj1463  33208  cdleme25cv  35172  cdleme40v  35283
  Copyright terms: Public domain W3C validator