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

Theorem cbvralv 2924
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 1629 . 2  |-  F/ y
ph
2 nfv 1629 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2920 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 2697
This theorem is referenced by:  cbvral2v  2932  cbvral3v  2934  reu7  3121  disjxun  4202  wereu2  4571  reusv3i  4722  dfwe2  4754  tfinds  4831  cnvpo  5402  f1mpt  5999  grprinvlem  6277  grprinvd  6278  tfrlem1  6628  tfrlem12  6642  rdglem1  6665  tz7.48lem  6690  nneneq  7282  marypha1lem  7430  supub  7454  suplub  7455  supmaxlem  7459  ordtypecbv  7476  ordtypelem3  7479  ordtypelem9  7485  wemaplem1  7505  brwdom3  7540  tcrank  7798  infxpenc2  7893  aceq1  7988  aceq2  7990  dfac5  7999  dfac9  8006  dfac12lem3  8015  kmlem12  8031  kmlem14  8033  cofsmo  8139  infpssrlem4  8176  isfin3ds  8199  isf32lem2  8224  isf32lem11  8233  isf33lem  8236  domtriomlem  8312  axdc3  8324  zorn2lem7  8372  zorn2g  8373  fpwwe2cbv  8495  fpwwecbv  8509  pwfseq  8529  axgroth6  8693  suprleub  9962  infmrgelb  9978  nnsub  10028  uzwo  10529  uzwoOLD  10530  ublbneg  10550  zsupss  10555  xrub  10880  monoord2  11344  faclbnd4lem4  11577  bccl  11603  hashbc  11692  wrdind  11781  cau3lem  12148  climmpt2  12357  caucvgrlem  12456  caurcvg2  12461  caucvgb  12463  fsum0diag2  12556  incexclem  12606  cvgrat  12650  mertenslem2  12652  mertens  12653  sqr2irr  12838  gcdcllem1  13001  prmind2  13080  prmpwdvds  13262  prmreclem5  13278  prmreclem6  13279  vdwlem7  13345  vdwlem10  13348  vdwlem13  13351  vdwnn  13356  ramcl  13387  isacs2  13868  catpropd  13925  spwmo  14648  gsumvalx  14764  issubg4  14951  isnsg2  14960  elnmz  14969  efgsdm  15352  pgpfac1lem5  15627  pgpfac1  15628  pgpfac  15632  ablfaclem3  15635  lbsextg  16224  evlslem2  16558  elcls3  17137  isclo2  17142  neiptopnei  17186  tgcn  17306  subbascn  17308  txcmplem2  17664  kqfvima  17752  kqt0lem  17758  isr0  17759  r0cld  17760  regr1lem2  17762  fbun  17862  flftg  18018  fclsbas  18043  alexsubALTlem2  18069  alexsubALTlem4  18071  ptcmplem4  18076  tsmsxplem1  18172  tsmsxp  18174  ustuqtop  18266  utopsnneip  18268  prdsxmslem2  18549  iscau4  19222  caucfil  19226  iscmet3  19236  bcthlem5  19271  bcth  19272  ovolicc2lem5  19407  uniioombllem6  19470  vitali  19495  ismbf3d  19536  itg1climres  19596  itg2seq  19624  itg2monolem1  19632  itg2mono  19635  rolle  19864  dvlipcn  19868  dvivthlem1  19882  mpfind  19955  ply1divex  20049  fta1g  20080  dgrco  20183  plydivex  20204  fta1  20215  vieta1  20219  ulmcaulem  20300  ulmcau  20301  abelthlem8  20345  wilth  20844  fta  20852  dchrelbas3  21012  2sqlem6  21143  2sqlem10  21148  dchrisumlem3  21175  dchrisum  21176  dchrmusumlema  21177  dchrvmasumlema  21184  dchrisum0lema  21198  pntibndlem3  21276  pntlem3  21293  pntleml  21295  pnt3  21296  ostth2lem2  21318  ostth  21323  cusgrafilem2  21479  grpoideu  21787  ubthlem3  22364  adjsym  23326  lnopunilem1  23503  elunop2  23506  lnophm  23512  cnlnadjlem5  23564  mdbr3  23790  mdbr4  23791  dmdbr3  23798  dmdbr4  23799  mddmd2  23802  toslub  24181  tosglb  24182  lmdvg  24328  esumcvg  24466  derangenlem  24847  subfacp1lem6  24861  subfacp1  24862  rescon  24923  cvmscbv  24935  untangtr  25153  dedekind  25177  dfon2lem3  25400  dfon2lem7  25404  cbvsetlike  25441  wfrlem1  25523  frrlem1  25547  axcontlem1  25868  axcontlem6  25873  mblfinlem  26207  ovoliunnfl  26211  voliunnfl  26213  mbfresfi  26216  nn0prpwlem  26279  neibastop3  26345  fnemeet2  26350  upixp  26385  sdclem2  26400  fdc  26403  mettrifi  26417  heiborlem5  26478  heiborlem10  26483  heibor  26484  bfp  26487  mzpclval  26736  dford3lem1  27051  fnwe2lem1  27079  aomclem3  27085  aomclem4  27086  aomclem8  27091  dfac11  27092  hbtlem5  27264  psgnunilem5  27349  psgnunilem3  27351  fnchoice  27631  cncmpmax  27634  climsuse  27665  stoweidlem7  27687  stoweidlem15  27695  stoweidlem35  27715  wallispilem3  27747  bnj1185  29066  bnj1379  29103  bnj222  29155  bnj517  29157  bnj1450  29320  bnj1452  29322  bnj1463  29325  cdleme25cv  31056  cdleme40v  31167
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702
  Copyright terms: Public domain W3C validator