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

Theorem cbvralv 2766
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 1607 . 2  |-  F/ y
ph
2 nfv 1607 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2762 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wral 2545
This theorem is referenced by:  cbvral2v  2774  cbvral3v  2776  reu7  2962  disjxun  4023  wereu2  4392  reusv3i  4543  dfwe2  4575  tfinds  4652  cnvpo  5215  f1mpt  5787  grprinvlem  6060  grprinvd  6061  tfrlem1  6393  tfrlem12  6407  rdglem1  6430  tz7.48lem  6455  nneneq  7046  marypha1lem  7188  supub  7212  suplub  7213  supmaxlem  7217  ordtypecbv  7234  ordtypelem3  7237  ordtypelem9  7243  wemaplem1  7263  brwdom3  7298  tcrank  7556  infxpenc2  7651  aceq1  7746  aceq2  7748  dfac5  7757  dfac9  7764  dfac12lem3  7773  kmlem12  7789  kmlem14  7791  cofsmo  7897  infpssrlem4  7934  isfin3ds  7957  isf32lem2  7982  isf32lem11  7991  isf33lem  7994  domtriomlem  8070  axdc3  8082  zorn2lem7  8131  zorn2g  8132  fpwwe2cbv  8254  fpwwecbv  8268  pwfseq  8288  axgroth6  8452  suprleub  9720  infmrgelb  9736  nnsub  9786  uzwo  10283  uzwoOLD  10284  ublbneg  10304  zsupss  10309  xrub  10632  monoord2  11079  faclbnd4lem4  11311  bccl  11336  hashbc  11393  wrdind  11479  cau3lem  11840  climmpt2  12049  caucvgrlem  12147  caurcvg2  12152  caucvgb  12154  fsum0diag2  12247  incexclem  12297  cvgrat  12341  mertenslem2  12343  mertens  12344  sqr2irr  12529  gcdcllem1  12692  prmind2  12771  prmpwdvds  12953  prmreclem5  12969  prmreclem6  12970  vdwlem7  13036  vdwlem10  13039  vdwlem13  13042  vdwnn  13047  ramcl  13078  isacs2  13557  catpropd  13614  spwmo  14337  gsumvalx  14453  issubg4  14640  isnsg2  14649  elnmz  14658  efgsdm  15041  pgpfac1lem5  15316  pgpfac1  15317  pgpfac  15321  ablfaclem3  15324  lbsextg  15917  evlslem2  16251  elcls3  16822  isclo2  16827  tgcn  16984  subbascn  16986  txcmplem2  17338  kqfvima  17423  kqt0lem  17429  isr0  17430  r0cld  17431  regr1lem2  17433  fbun  17537  flftg  17693  fclsbas  17718  alexsubALTlem2  17744  alexsubALTlem4  17746  ptcmplem4  17751  tsmsxplem1  17837  tsmsxp  17839  prdsxmslem2  18077  iscau4  18707  caucfil  18711  iscmet3  18721  bcthlem5  18752  bcth  18753  ovolicc2lem5  18882  uniioombllem6  18945  vitali  18970  ismbf3d  19011  itg1climres  19071  itg2seq  19099  itg2monolem1  19107  itg2mono  19110  rolle  19339  dvlipcn  19343  dvivthlem1  19357  mpfind  19430  ply1divex  19524  fta1g  19555  dgrco  19658  plydivex  19679  fta1  19690  vieta1  19694  ulmcaulem  19773  ulmcau  19774  abelthlem8  19817  wilth  20311  fta  20319  dchrelbas3  20479  2sqlem6  20610  2sqlem10  20615  dchrisumlem3  20642  dchrisum  20643  dchrmusumlema  20644  dchrvmasumlema  20651  dchrisum0lema  20665  pntibndlem3  20743  pntlem3  20760  pntleml  20762  pnt3  20763  ostth2lem2  20785  ostth  20790  grpoideu  20878  ubthlem3  21453  adjsym  22415  lnopunilem1  22592  elunop2  22595  lnophm  22601  cnlnadjlem5  22653  mdbr3  22879  mdbr4  22880  dmdbr3  22887  dmdbr4  22888  mddmd2  22891  esumcvg  23456  derangenlem  23704  subfacp1lem6  23718  subfacp1  23719  rescon  23779  cvmscbv  23791  untangtr  24062  dedekind  24084  dfon2lem3  24143  dfon2lem7  24147  cbvsetlike  24183  wfrlem1  24258  tfr3ALT  24281  frrlem1  24283  axcontlem1  24594  axcontlem6  24599  bpolyval  24786  celsor  25122  nn0prpwlem  26249  neibastop3  26322  fnemeet2  26327  upixp  26414  sdclem2  26463  fdc  26466  mettrifi  26484  heiborlem5  26550  heiborlem10  26555  heibor  26556  bfp  26559  mzpclval  26814  dford3lem1  27130  fnwe2lem1  27158  aomclem3  27164  aomclem4  27165  aomclem8  27170  dfac11  27171  hbtlem5  27343  psgnunilem5  27428  psgnunilem3  27430  fnchoice  27711  cncmpmax  27714  stoweidlem35  27795  bnj1185  28899  bnj1379  28936  bnj222  28988  bnj517  28990  bnj1450  29153  bnj1452  29155  bnj1463  29158  cdleme25cv  30620  cdleme40v  30731
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550
  Copyright terms: Public domain W3C validator