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

Theorem cbvralv 2875
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 1626 . 2  |-  F/ y
ph
2 nfv 1626 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2871 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wral 2649
This theorem is referenced by:  cbvral2v  2883  cbvral3v  2885  reu7  3072  disjxun  4151  wereu2  4520  reusv3i  4670  dfwe2  4702  tfinds  4779  cnvpo  5350  f1mpt  5946  grprinvlem  6224  grprinvd  6225  tfrlem1  6572  tfrlem12  6586  rdglem1  6609  tz7.48lem  6634  nneneq  7226  marypha1lem  7373  supub  7397  suplub  7398  supmaxlem  7402  ordtypecbv  7419  ordtypelem3  7422  ordtypelem9  7428  wemaplem1  7448  brwdom3  7483  tcrank  7741  infxpenc2  7836  aceq1  7931  aceq2  7933  dfac5  7942  dfac9  7949  dfac12lem3  7958  kmlem12  7974  kmlem14  7976  cofsmo  8082  infpssrlem4  8119  isfin3ds  8142  isf32lem2  8167  isf32lem11  8176  isf33lem  8179  domtriomlem  8255  axdc3  8267  zorn2lem7  8315  zorn2g  8316  fpwwe2cbv  8438  fpwwecbv  8452  pwfseq  8472  axgroth6  8636  suprleub  9904  infmrgelb  9920  nnsub  9970  uzwo  10471  uzwoOLD  10472  ublbneg  10492  zsupss  10497  xrub  10822  monoord2  11281  faclbnd4lem4  11514  bccl  11540  hashbc  11629  wrdind  11718  cau3lem  12085  climmpt2  12294  caucvgrlem  12393  caurcvg2  12398  caucvgb  12400  fsum0diag2  12493  incexclem  12543  cvgrat  12587  mertenslem2  12589  mertens  12590  sqr2irr  12775  gcdcllem1  12938  prmind2  13017  prmpwdvds  13199  prmreclem5  13215  prmreclem6  13216  vdwlem7  13282  vdwlem10  13285  vdwlem13  13288  vdwnn  13293  ramcl  13324  isacs2  13805  catpropd  13862  spwmo  14585  gsumvalx  14701  issubg4  14888  isnsg2  14897  elnmz  14906  efgsdm  15289  pgpfac1lem5  15564  pgpfac1  15565  pgpfac  15569  ablfaclem3  15572  lbsextg  16161  evlslem2  16495  elcls3  17070  isclo2  17075  neiptopnei  17119  tgcn  17238  subbascn  17240  txcmplem2  17595  kqfvima  17683  kqt0lem  17689  isr0  17690  r0cld  17691  regr1lem2  17693  fbun  17793  flftg  17949  fclsbas  17974  alexsubALTlem2  18000  alexsubALTlem4  18002  ptcmplem4  18007  tsmsxplem1  18103  tsmsxp  18105  ustuqtop  18197  utopsnneip  18199  prdsxmslem2  18449  iscau4  19103  caucfil  19107  iscmet3  19117  bcthlem5  19150  bcth  19151  ovolicc2lem5  19284  uniioombllem6  19347  vitali  19372  ismbf3d  19413  itg1climres  19473  itg2seq  19501  itg2monolem1  19509  itg2mono  19512  rolle  19741  dvlipcn  19745  dvivthlem1  19759  mpfind  19832  ply1divex  19926  fta1g  19957  dgrco  20060  plydivex  20081  fta1  20092  vieta1  20096  ulmcaulem  20177  ulmcau  20178  abelthlem8  20222  wilth  20721  fta  20729  dchrelbas3  20889  2sqlem6  21020  2sqlem10  21025  dchrisumlem3  21052  dchrisum  21053  dchrmusumlema  21054  dchrvmasumlema  21061  dchrisum0lema  21075  pntibndlem3  21153  pntlem3  21170  pntleml  21172  pnt3  21173  ostth2lem2  21195  ostth  21200  cusgrafilem2  21355  grpoideu  21645  ubthlem3  22222  adjsym  23184  lnopunilem1  23361  elunop2  23364  lnophm  23370  cnlnadjlem5  23422  mdbr3  23648  mdbr4  23649  dmdbr3  23656  dmdbr4  23657  mddmd2  23660  lmdvg  24142  esumcvg  24272  derangenlem  24636  subfacp1lem6  24650  subfacp1  24651  rescon  24712  cvmscbv  24724  untangtr  24942  dedekind  24966  dfon2lem3  25165  dfon2lem7  25169  cbvsetlike  25205  wfrlem1  25280  tfr3ALT  25303  frrlem1  25305  axcontlem1  25617  axcontlem6  25622  bpolyval  25809  ovoliunnfl  25953  voliunnfl  25955  nn0prpwlem  26016  neibastop3  26082  fnemeet2  26087  upixp  26122  sdclem2  26137  fdc  26140  mettrifi  26154  heiborlem5  26215  heiborlem10  26220  heibor  26221  bfp  26224  mzpclval  26473  dford3lem1  26788  fnwe2lem1  26816  aomclem3  26822  aomclem4  26823  aomclem8  26828  dfac11  26829  hbtlem5  27001  psgnunilem5  27086  psgnunilem3  27088  fnchoice  27368  cncmpmax  27371  climsuse  27402  stoweidlem7  27424  stoweidlem15  27432  stoweidlem35  27452  wallispilem3  27484  bnj1185  28503  bnj1379  28540  bnj222  28592  bnj517  28594  bnj1450  28757  bnj1452  28759  bnj1463  28762  cdleme25cv  30472  cdleme40v  30583
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654
  Copyright terms: Public domain W3C validator