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

Theorem cbvralv 2937
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 1672 . 2  |-  F/ y
ph
2 nfv 1672 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2933 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710
This theorem is referenced by:  cbvral2v  2945  cbvral3v  2947  reu7  3143  disjxun  4278  reusv3i  4487  wereu2  4704  cnvpo  5363  f1mpt  5961  grprinvlem  6290  grprinvd  6291  dfwe2  6382  tfinds  6459  tfrlem1  6821  tfrlem12  6834  rdglem1  6857  tz7.48lem  6882  nneneq  7482  marypha1lem  7671  supub  7697  suplub  7698  supmaxlem  7702  ordtypecbv  7719  ordtypelem3  7722  ordtypelem9  7728  wemaplem1  7748  brwdom3  7785  tcrank  8079  infxpenc2  8176  infxpenc2OLD  8180  aceq1  8275  aceq2  8277  dfac5  8286  dfac9  8293  dfac12lem3  8302  kmlem12  8318  kmlem14  8320  cofsmo  8426  infpssrlem4  8463  isfin3ds  8486  isf32lem2  8511  isf32lem11  8520  isf33lem  8523  domtriomlem  8599  axdc3  8611  zorn2lem7  8659  zorn2g  8660  fpwwe2cbv  8784  fpwwecbv  8798  pwfseq  8818  axgroth6  8982  dedekind  9520  suprleub  10281  infmrgelb  10297  nnsub  10347  uzwo  10904  uzwoOLD  10905  ublbneg  10926  zsupss  10931  xrub  11261  monoord2  11820  faclbnd4lem4  12055  bccl  12081  hashbc  12189  wrdind  12354  wrd2ind  12355  cau3lem  12825  climmpt2  13034  caucvgrlem  13133  caurcvg2  13138  caucvgb  13140  fsum0diag2  13232  incexclem  13281  cvgrat  13325  mertenslem2  13327  mertens  13328  sqr2irr  13513  gcdcllem1  13677  prmind2  13756  prmpwdvds  13947  prmreclem5  13963  prmreclem6  13964  vdwlem7  14030  vdwlem10  14033  vdwlem13  14036  vdwnn  14041  ramcl  14072  isacs2  14573  catpropd  14630  mrcmndind  15475  gsumvalx  15483  issubg4  15679  isnsg2  15690  elnmz  15699  gsmsymgreqlem2  15915  psgnunilem5  15979  psgnunilem3  15981  efgsdm  16206  pgpfac1lem5  16553  pgpfac1  16554  pgpfac  16558  ablfaclem3  16561  lbsextg  17164  evlslem2  17524  mdetuni0  18268  elcls3  18528  isclo2  18533  neiptopnei  18577  tgcn  18697  subbascn  18699  txcmplem2  19056  kqfvima  19144  kqt0lem  19150  isr0  19151  r0cld  19152  regr1lem2  19154  fbun  19254  flftg  19410  fclsbas  19435  alexsubALTlem2  19461  alexsubALTlem4  19463  ptcmplem4  19468  tsmsxplem1  19568  tsmsxp  19570  ustuqtop  19662  utopsnneip  19664  prdsxmslem2  19945  iscau4  20631  caucfil  20635  iscmet3  20645  bcthlem5  20680  bcth  20681  ovolicc2lem5  20845  uniioombllem6  20909  vitali  20934  ismbf3d  20973  itg1climres  21033  itg2seq  21061  itg2monolem1  21069  itg2mono  21072  rolle  21303  dvlipcn  21307  dvivthlem1  21321  mpfind  21395  ply1divex  21492  fta1g  21523  dgrco  21626  plydivex  21647  fta1  21658  vieta1  21662  ulmcaulem  21743  ulmcau  21744  abelthlem8  21788  wilth  22293  fta  22301  dchrelbas3  22461  2sqlem6  22592  2sqlem10  22597  dchrisumlem3  22624  dchrisum  22625  dchrmusumlema  22626  dchrvmasumlema  22633  dchrisum0lema  22647  pntibndlem3  22725  pntlem3  22742  pntleml  22744  pnt3  22745  ostth2lem2  22767  ostth  22772  axcontlem1  23032  axcontlem6  23037  cusgrafilem2  23210  grpoideu  23518  ubthlem3  24095  adjsym  25059  lnopunilem1  25236  elunop2  25239  lnophm  25245  cnlnadjlem5  25297  mdbr3  25523  mdbr4  25524  dmdbr3  25531  dmdbr4  25532  mddmd2  25535  toslublem  25950  tosglblem  25952  archiabl  26038  isarchiofld  26137  lmdvg  26236  esumcvg  26388  eulerpartlemsv3  26591  eulerpartlemgvv  26606  signstfvneq0  26820  derangenlem  26906  subfacp1lem6  26920  subfacp1  26921  rescon  26982  cvmscbv  26994  untangtr  27211  dfon2lem3  27444  dfon2lem7  27448  cbvsetlike  27488  wfrlem1  27570  frrlem1  27614  heicant  28267  mblfinlem2  28270  ovoliunnfl  28274  voliunnfl  28276  mbfresfi  28279  nn0prpwlem  28358  neibastop3  28424  fnemeet2  28429  upixp  28464  sdclem2  28479  fdc  28482  mettrifi  28494  heiborlem5  28555  heiborlem10  28560  heibor  28561  bfp  28564  mzpclval  28903  dford3lem1  29217  fnwe2lem1  29245  aomclem3  29251  aomclem4  29252  aomclem8  29256  dfac11  29257  hbtlem5  29326  fnchoice  29593  cncmpmax  29596  climsuse  29624  stoweidlem7  29645  stoweidlem15  29653  stoweidlem35  29673  wallispilem3  29705  reuccats1  30104  usg2wlkeq  30132  bnj1185  31486  bnj1379  31523  bnj222  31575  bnj517  31577  bnj1450  31740  bnj1452  31742  bnj1463  31745  cdleme25cv  33572  cdleme40v  33683
  Copyright terms: Public domain W3C validator