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  7456  suplub  7457  supmaxlem  7461  ordtypecbv  7478  ordtypelem3  7481  ordtypelem9  7487  wemaplem1  7507  brwdom3  7542  tcrank  7800  infxpenc2  7895  aceq1  7990  aceq2  7992  dfac5  8001  dfac9  8008  dfac12lem3  8017  kmlem12  8033  kmlem14  8035  cofsmo  8141  infpssrlem4  8178  isfin3ds  8201  isf32lem2  8226  isf32lem11  8235  isf33lem  8238  domtriomlem  8314  axdc3  8326  zorn2lem7  8374  zorn2g  8375  fpwwe2cbv  8497  fpwwecbv  8511  pwfseq  8531  axgroth6  8695  suprleub  9964  infmrgelb  9980  nnsub  10030  uzwo  10531  uzwoOLD  10532  ublbneg  10552  zsupss  10557  xrub  10882  monoord2  11346  faclbnd4lem4  11579  bccl  11605  hashbc  11694  wrdind  11783  cau3lem  12150  climmpt2  12359  caucvgrlem  12458  caurcvg2  12463  caucvgb  12465  fsum0diag2  12558  incexclem  12608  cvgrat  12652  mertenslem2  12654  mertens  12655  sqr2irr  12840  gcdcllem1  13003  prmind2  13082  prmpwdvds  13264  prmreclem5  13280  prmreclem6  13281  vdwlem7  13347  vdwlem10  13350  vdwlem13  13353  vdwnn  13358  ramcl  13389  isacs2  13870  catpropd  13927  spwmo  14650  gsumvalx  14766  issubg4  14953  isnsg2  14962  elnmz  14971  efgsdm  15354  pgpfac1lem5  15629  pgpfac1  15630  pgpfac  15634  ablfaclem3  15637  lbsextg  16226  evlslem2  16560  elcls3  17139  isclo2  17144  neiptopnei  17188  tgcn  17308  subbascn  17310  txcmplem2  17666  kqfvima  17754  kqt0lem  17760  isr0  17761  r0cld  17762  regr1lem2  17764  fbun  17864  flftg  18020  fclsbas  18045  alexsubALTlem2  18071  alexsubALTlem4  18073  ptcmplem4  18078  tsmsxplem1  18174  tsmsxp  18176  ustuqtop  18268  utopsnneip  18270  prdsxmslem2  18551  iscau4  19224  caucfil  19228  iscmet3  19238  bcthlem5  19273  bcth  19274  ovolicc2lem5  19409  uniioombllem6  19472  vitali  19497  ismbf3d  19538  itg1climres  19598  itg2seq  19626  itg2monolem1  19634  itg2mono  19637  rolle  19866  dvlipcn  19870  dvivthlem1  19884  mpfind  19957  ply1divex  20051  fta1g  20082  dgrco  20185  plydivex  20206  fta1  20217  vieta1  20221  ulmcaulem  20302  ulmcau  20303  abelthlem8  20347  wilth  20846  fta  20854  dchrelbas3  21014  2sqlem6  21145  2sqlem10  21150  dchrisumlem3  21177  dchrisum  21178  dchrmusumlema  21179  dchrvmasumlema  21186  dchrisum0lema  21200  pntibndlem3  21278  pntlem3  21295  pntleml  21297  pnt3  21298  ostth2lem2  21320  ostth  21325  cusgrafilem2  21481  grpoideu  21789  ubthlem3  22366  adjsym  23328  lnopunilem1  23505  elunop2  23508  lnophm  23514  cnlnadjlem5  23566  mdbr3  23792  mdbr4  23793  dmdbr3  23800  dmdbr4  23801  mddmd2  23804  toslub  24183  tosglb  24184  lmdvg  24330  esumcvg  24468  derangenlem  24849  subfacp1lem6  24863  subfacp1  24864  rescon  24925  cvmscbv  24937  untangtr  25155  dedekind  25179  dfon2lem3  25404  dfon2lem7  25408  cbvsetlike  25448  wfrlem1  25530  frrlem1  25574  axcontlem1  25895  axcontlem6  25900  mblfinlem  26234  ovoliunnfl  26238  voliunnfl  26240  mbfresfi  26243  nn0prpwlem  26316  neibastop3  26382  fnemeet2  26387  upixp  26422  sdclem2  26437  fdc  26440  mettrifi  26454  heiborlem5  26515  heiborlem10  26520  heibor  26521  bfp  26524  mzpclval  26773  dford3lem1  27088  fnwe2lem1  27116  aomclem3  27122  aomclem4  27123  aomclem8  27127  dfac11  27128  hbtlem5  27300  psgnunilem5  27385  psgnunilem3  27387  fnchoice  27667  cncmpmax  27670  climsuse  27701  stoweidlem7  27723  stoweidlem15  27731  stoweidlem35  27751  wallispilem3  27783  bnj1185  29102  bnj1379  29139  bnj222  29191  bnj517  29193  bnj1450  29356  bnj1452  29358  bnj1463  29361  cdleme25cv  31092  cdleme40v  31203
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