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

Theorem cbvralv 2934
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 1630 . 2  |-  F/ y
ph
2 nfv 1630 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2930 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wral 2707
This theorem is referenced by:  cbvral2v  2942  cbvral3v  2944  reu7  3131  disjxun  4213  wereu2  4582  reusv3i  4733  dfwe2  4765  tfinds  4842  cnvpo  5413  f1mpt  6010  grprinvlem  6288  grprinvd  6289  tfrlem1  6639  tfrlem12  6653  rdglem1  6676  tz7.48lem  6701  nneneq  7293  marypha1lem  7441  supub  7467  suplub  7468  supmaxlem  7472  ordtypecbv  7489  ordtypelem3  7492  ordtypelem9  7498  wemaplem1  7518  brwdom3  7553  tcrank  7813  infxpenc2  7908  aceq1  8003  aceq2  8005  dfac5  8014  dfac9  8021  dfac12lem3  8030  kmlem12  8046  kmlem14  8048  cofsmo  8154  infpssrlem4  8191  isfin3ds  8214  isf32lem2  8239  isf32lem11  8248  isf33lem  8251  domtriomlem  8327  axdc3  8339  zorn2lem7  8387  zorn2g  8388  fpwwe2cbv  8510  fpwwecbv  8524  pwfseq  8544  axgroth6  8708  suprleub  9977  infmrgelb  9993  nnsub  10043  uzwo  10544  uzwoOLD  10545  ublbneg  10565  zsupss  10570  xrub  10895  monoord2  11359  faclbnd4lem4  11592  bccl  11618  hashbc  11707  wrdind  11796  cau3lem  12163  climmpt2  12372  caucvgrlem  12471  caurcvg2  12476  caucvgb  12478  fsum0diag2  12571  incexclem  12621  cvgrat  12665  mertenslem2  12667  mertens  12668  sqr2irr  12853  gcdcllem1  13016  prmind2  13095  prmpwdvds  13277  prmreclem5  13293  prmreclem6  13294  vdwlem7  13360  vdwlem10  13363  vdwlem13  13366  vdwnn  13371  ramcl  13402  isacs2  13883  catpropd  13940  spwmo  14663  gsumvalx  14779  issubg4  14966  isnsg2  14975  elnmz  14984  efgsdm  15367  pgpfac1lem5  15642  pgpfac1  15643  pgpfac  15647  ablfaclem3  15650  lbsextg  16239  evlslem2  16573  elcls3  17152  isclo2  17157  neiptopnei  17201  tgcn  17321  subbascn  17323  txcmplem2  17679  kqfvima  17767  kqt0lem  17773  isr0  17774  r0cld  17775  regr1lem2  17777  fbun  17877  flftg  18033  fclsbas  18058  alexsubALTlem2  18084  alexsubALTlem4  18086  ptcmplem4  18091  tsmsxplem1  18187  tsmsxp  18189  ustuqtop  18281  utopsnneip  18283  prdsxmslem2  18564  iscau4  19237  caucfil  19241  iscmet3  19251  bcthlem5  19286  bcth  19287  ovolicc2lem5  19422  uniioombllem6  19485  vitali  19510  ismbf3d  19549  itg1climres  19609  itg2seq  19637  itg2monolem1  19645  itg2mono  19648  rolle  19879  dvlipcn  19883  dvivthlem1  19897  mpfind  19970  ply1divex  20064  fta1g  20095  dgrco  20198  plydivex  20219  fta1  20230  vieta1  20234  ulmcaulem  20315  ulmcau  20316  abelthlem8  20360  wilth  20859  fta  20867  dchrelbas3  21027  2sqlem6  21158  2sqlem10  21163  dchrisumlem3  21190  dchrisum  21191  dchrmusumlema  21192  dchrvmasumlema  21199  dchrisum0lema  21213  pntibndlem3  21291  pntlem3  21308  pntleml  21310  pnt3  21311  ostth2lem2  21333  ostth  21338  cusgrafilem2  21494  grpoideu  21802  ubthlem3  22379  adjsym  23341  lnopunilem1  23518  elunop2  23521  lnophm  23527  cnlnadjlem5  23579  mdbr3  23805  mdbr4  23806  dmdbr3  23813  dmdbr4  23814  mddmd2  23817  toslub  24196  tosglb  24197  lmdvg  24343  esumcvg  24481  derangenlem  24862  subfacp1lem6  24876  subfacp1  24877  rescon  24938  cvmscbv  24950  untangtr  25168  dedekind  25192  dfon2lem3  25417  dfon2lem7  25421  cbvsetlike  25461  wfrlem1  25543  frrlem1  25587  axcontlem1  25908  axcontlem6  25913  heicant  26253  mblfinlem2  26256  ovoliunnfl  26260  voliunnfl  26262  mbfresfi  26265  nn0prpwlem  26339  neibastop3  26405  fnemeet2  26410  upixp  26445  sdclem2  26460  fdc  26463  mettrifi  26477  heiborlem5  26538  heiborlem10  26543  heibor  26544  bfp  26547  mzpclval  26796  dford3lem1  27111  fnwe2lem1  27139  aomclem3  27145  aomclem4  27146  aomclem8  27150  dfac11  27151  hbtlem5  27323  psgnunilem5  27408  psgnunilem3  27410  fnchoice  27690  cncmpmax  27693  climsuse  27724  stoweidlem7  27746  stoweidlem15  27754  stoweidlem35  27774  wallispilem3  27806  usg2wlkeq  28342  bnj1185  29239  bnj1379  29276  bnj222  29328  bnj517  29330  bnj1450  29493  bnj1452  29495  bnj1463  29498  cdleme25cv  31229  cdleme40v  31340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712
  Copyright terms: Public domain W3C validator