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

Theorem cbvralv 3033
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 1728 . 2  |-  F/ y
ph
2 nfv 1728 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 3029 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 2753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1634  df-nf 1638  df-sb 1764  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2758
This theorem is referenced by:  cbvral2v  3041  cbvral3v  3043  reu7  3243  disjxun  4392  reusv3i  4600  wereu2  4819  cnvpo  5361  f1mpt  6149  grprinvlem  6493  grprinvd  6494  dfwe2  6598  tfinds  6676  wfrlem1  7019  tfrlem1  7078  tfrlem12  7091  rdglem1  7117  tz7.48lem  7142  nneneq  7737  marypha1lem  7926  supub  7951  suplub  7952  supmaxlemOLD  7957  ordtypecbv  7975  ordtypelem3  7978  ordtypelem9  7984  wemaplem1  8004  brwdom3  8041  tcrank  8333  infxpenc2  8430  infxpenc2OLD  8434  aceq1  8529  aceq2  8531  dfac5  8540  dfac9  8547  dfac12lem3  8556  kmlem12  8572  kmlem14  8574  cofsmo  8680  infpssrlem4  8717  isfin3ds  8740  isf32lem2  8765  isf32lem11  8774  isf33lem  8777  domtriomlem  8853  axdc3  8865  zorn2lem7  8913  zorn2g  8914  fpwwe2cbv  9037  fpwwecbv  9051  pwfseq  9071  axgroth6  9235  dedekind  9777  suprleub  10546  infmrgelb  10562  nnsub  10614  uzwo  11189  ublbneg  11210  zsupss  11215  xrub  11555  fsuppmapnn0fiubex  12140  monoord2  12180  faclbnd4lem4  12416  bccl  12442  hashbc  12549  wrdind  12756  wrd2ind  12757  reuccats1  12760  cau3lem  13334  climmpt2  13543  caucvgrlem  13642  caurcvg2  13647  caucvgb  13649  fsum0diag2  13747  incexclem  13797  cvgrat  13842  mertenslem2  13844  mertens  13845  sqrt2irr  14189  gcdcllem1  14356  prmind2  14435  prmpwdvds  14629  prmreclem5  14645  prmreclem6  14646  vdwlem7  14712  vdwlem10  14715  vdwlem13  14718  vdwnn  14723  ramcl  14754  isacs2  15265  catpropd  15320  gsumvalx  16219  mrcmndind  16319  issubg4  16542  isnsg2  16553  elnmz  16562  gsmsymgreqlem2  16778  psgnunilem5  16841  psgnunilem3  16843  efgsdm  17070  gsummptnn0fzfv  17334  pgpfac1lem5  17448  pgpfac1  17449  pgpfac  17453  ablfaclem3  17456  lbsextg  18126  evlslem2  18498  mpfind  18523  cply1mul  18653  mdetuni0  19413  m2cpminvid2lem  19545  mp2pm2mplem4  19600  chcoeffeqlem  19676  cayhamlem3  19678  elcls3  19875  isclo2  19880  neiptopnei  19924  tgcn  20044  subbascn  20046  txcmplem2  20433  kqfvima  20521  kqt0lem  20527  isr0  20528  r0cld  20529  regr1lem2  20531  fbun  20631  flftg  20787  fclsbas  20812  alexsubALTlem2  20838  alexsubALTlem4  20840  ptcmplem4  20845  tsmsxplem1  20945  tsmsxp  20947  ustuqtop  21039  utopsnneip  21041  prdsxmslem2  21322  iscau4  22008  caucfil  22012  iscmet3  22022  bcthlem5  22057  bcth  22058  ovolicc2lem5  22222  uniioombllem6  22287  vitali  22312  ismbf3d  22351  itg1climres  22411  itg2seq  22439  itg2monolem1  22447  itg2mono  22450  rolle  22681  dvlipcn  22685  dvivthlem1  22699  ply1divex  22827  fta1g  22858  dgrco  22962  plydivex  22983  fta1  22994  vieta1  22998  ulmcaulem  23079  ulmcau  23080  abelthlem8  23124  wilth  23724  fta  23732  dchrelbas3  23892  2sqlem6  24023  2sqlem10  24028  dchrisumlem3  24055  dchrisum  24056  dchrmusumlema  24057  dchrvmasumlema  24064  dchrisum0lema  24078  pntibndlem3  24156  pntlem3  24173  pntleml  24175  pnt3  24176  ostth2lem2  24198  ostth  24203  axcontlem1  24671  axcontlem6  24676  cusgrafilem2  24884  usg2wlkeq  25112  grpoideu  25611  ubthlem3  26188  adjsym  27151  lnopunilem1  27328  elunop2  27331  lnophm  27337  cnlnadjlem5  27389  mdbr3  27615  mdbr4  27616  dmdbr3  27623  dmdbr4  27624  mddmd2  27627  toslublem  28093  tosglblem  28095  archiabl  28180  isarchiofld  28246  qtophaus  28278  lmdvg  28374  esumcvg  28519  unelldsys  28592  ldgenpisyslem1  28597  eulerpartlemsv3  28792  eulerpartlemgvv  28807  signstfvneq0  29021  bnj1185  29166  bnj1379  29203  bnj222  29255  bnj517  29257  bnj1450  29420  bnj1452  29422  bnj1463  29425  derangenlem  29455  subfacp1lem6  29469  subfacp1  29470  rescon  29530  cvmscbv  29542  untangtr  29902  dfon2lem3  29991  dfon2lem7  29995  frrlem1  30074  nn0prpwlem  30537  neibastop3  30577  fnemeet2  30582  heicant  31401  mblfinlem2  31404  ovoliunnfl  31408  voliunnfl  31410  mbfresfi  31413  upixp  31482  sdclem2  31497  fdc  31500  mettrifi  31512  heiborlem5  31573  heiborlem10  31578  heibor  31579  bfp  31582  cdleme25cv  33357  cdleme40v  33468  mzpclval  34999  dford3lem1  35310  fnwe2lem1  35338  aomclem3  35344  aomclem4  35345  aomclem8  35349  dfac11  35350  hbtlem5  35421  fnchoice  36764  cncmpmax  36767  mccl  36955  climsuse  36963  limsupre  36996  dvbdfbdioolem2  37075  dvbdfbdioo  37076  ioodvbdlimc1lem1  37077  ioodvbdlimc1lem2  37078  ioodvbdlimc2lem  37080  dvnprodlem3  37094  stoweidlem7  37138  stoweidlem15  37146  stoweidlem35  37166  wallispilem3  37198  fourierdlem68  37306  fourierdlem71  37309  fourierdlem73  37311  fourierdlem87  37325  fourierdlem100  37338  fourierdlem103  37341  fourierdlem104  37342  fourierdlem107  37345  fourierdlem109  37347  fourierdlem112  37350  etransc  37415  bgoldbtbndlem4  37837  bgoldbtbnd  37838  nn0sumshdiglem1  38733
  Copyright terms: Public domain W3C validator