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

Theorem cbvralv 3031
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 1772 . 2  |-  F/ y
ph
2 nfv 1772 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 3027 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-ex 1675  df-nf 1679  df-sb 1809  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754
This theorem is referenced by:  cbvral2v  3039  cbvral3v  3041  reu7  3245  disjxun  4416  reusv3i  4627  wereu2  4853  cnvpo  5397  f1mpt  6192  grprinvlem  6539  grprinvd  6540  dfwe2  6640  tfinds  6718  wfrlem1  7066  tfrlem1  7125  tfrlem12  7138  rdglem1  7164  tz7.48lem  7189  nneneq  7786  marypha1lem  7978  supub  8004  suplub  8005  supmaxlemOLD  8013  ordtypecbv  8063  ordtypelem3  8066  ordtypelem9  8072  wemaplem1  8092  brwdom3  8128  tcrank  8386  infxpenc2  8484  aceq1  8579  aceq2  8581  dfac5  8590  dfac9  8597  dfac12lem3  8606  kmlem12  8622  kmlem14  8624  cofsmo  8730  infpssrlem4  8767  isfin3ds  8790  isf32lem2  8815  isf32lem11  8824  isf33lem  8827  domtriomlem  8903  axdc3  8915  zorn2lem7  8963  zorn2g  8964  fpwwe2cbv  9086  fpwwecbv  9100  pwfseq  9120  axgroth6  9284  dedekind  9828  suprleub  10606  infregelb  10627  infmrgelbOLD  10628  nnsub  10681  uzwo  11256  ublbneg  11282  zsupss  11287  xrub  11631  fsuppmapnn0fiubex  12242  monoord2  12282  faclbnd4lem4  12519  bccl  12545  hashbc  12655  wrdind  12876  wrd2ind  12877  reuccats1  12880  cau3lem  13472  climmpt2  13692  caucvgrlem  13791  caucvgrlemOLD  13792  caurcvg2  13799  caucvgb  13801  fsum0diag2  13899  incexclem  13949  cvgrat  13994  mertenslem2  13996  mertens  13997  sqrt2irr  14356  gcdcllem1  14528  lcmfunsnlem1  14665  lcmfunsnlem2lem1  14666  prmind2  14690  prmpwdvds  14903  prmreclem5  14919  prmreclem6  14920  vdwlem7  14992  vdwlem10  14995  vdwlem13  14998  vdwnn  15003  ramcl  15042  prmgaplcmlem1OLD  15067  prmordvdslcmsOLDOLD  15076  isacs2  15614  catpropd  15669  gsumvalx  16568  mrcmndind  16668  issubg4  16891  isnsg2  16902  elnmz  16911  gsmsymgreqlem2  17127  psgnunilem5  17190  psgnunilem3  17192  efgsdm  17435  gsummptnn0fzfv  17672  pgpfac1lem5  17767  pgpfac1  17768  pgpfac  17772  ablfaclem3  17775  lbsextg  18440  evlslem2  18790  mpfind  18814  cply1mul  18942  mdetuni0  19701  m2cpminvid2lem  19833  mp2pm2mplem4  19888  chcoeffeqlem  19964  cayhamlem3  19966  elcls3  20154  isclo2  20159  neiptopnei  20203  tgcn  20323  subbascn  20325  txcmplem2  20712  kqfvima  20800  kqt0lem  20806  isr0  20807  r0cld  20808  regr1lem2  20810  fbun  20910  flftg  21066  fclsbas  21091  alexsubALTlem2  21118  alexsubALTlem4  21120  ptcmplem4  21125  tsmsxplem1  21222  tsmsxp  21224  ustuqtop  21316  utopsnneip  21318  prdsxmslem2  21599  iscau4  22304  caucfil  22308  iscmet3  22318  bcthlem5  22351  bcth  22352  ovolicc2lem5  22530  uniioombllem6  22602  vitali  22627  ismbf3d  22666  itg1climres  22728  itg2seq  22756  itg2monolem1  22764  itg2mono  22767  rolle  22998  dvlipcn  23002  dvivthlem1  23016  ply1divex  23143  fta1g  23174  dgrco  23285  plydivex  23306  fta1  23317  vieta1  23321  ulmcaulem  23405  ulmcau  23406  abelthlem8  23450  wilth  24052  fta  24062  dchrelbas3  24222  2sqlem6  24353  2sqlem10  24358  dchrisumlem3  24385  dchrisum  24386  dchrmusumlema  24387  dchrvmasumlema  24394  dchrisum0lema  24408  pntibndlem3  24486  pntlem3  24503  pntleml  24505  pnt3  24506  ostth2lem2  24528  ostth  24533  axcontlem1  25050  axcontlem6  25055  cusgrafilem2  25264  usg2wlkeq  25492  grpoideu  25993  ubthlem3  26570  adjsym  27542  lnopunilem1  27719  elunop2  27722  lnophm  27728  cnlnadjlem5  27780  mdbr3  28006  mdbr4  28007  dmdbr3  28014  dmdbr4  28015  mddmd2  28018  toslublem  28480  tosglblem  28482  archiabl  28566  isarchiofld  28631  qtophaus  28714  lmdvg  28810  esumcvg  28958  unelldsys  29031  ldgenpisyslem1  29036  eulerpartlemsv3  29244  eulerpartlemgvv  29259  signstfvneq0  29511  bnj1185  29655  bnj1379  29692  bnj222  29744  bnj517  29746  bnj1450  29909  bnj1452  29911  bnj1463  29914  derangenlem  29944  subfacp1lem6  29958  subfacp1  29959  rescon  30019  cvmscbv  30031  untangtr  30391  dfon2lem3  30481  dfon2lem7  30485  frrlem1  30564  nn0prpwlem  31028  neibastop3  31068  fnemeet2  31073  phpreu  31975  poimirlem27  32013  heicant  32021  mblfinlem2  32024  ovoliunnfl  32028  voliunnfl  32030  mbfresfi  32033  upixp  32102  sdclem2  32117  fdc  32120  mettrifi  32132  heiborlem5  32193  heiborlem10  32198  heibor  32199  bfp  32202  cdleme25cv  33971  cdleme40v  34082  mzpclval  35613  dford3lem1  35927  fnwe2lem1  35954  aomclem3  35960  aomclem4  35961  aomclem8  35965  dfac11  35966  hbtlem5  36033  fnchoice  37391  cncmpmax  37394  wessf1ornlem  37513  disjinfi  37522  mccl  37764  climsuse  37773  limsupre  37807  limsupreOLD  37808  dvbdfbdioolem2  37887  dvbdfbdioo  37888  ioodvbdlimc1lem1  37889  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem1OLD  37891  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  dvnprodlem3  37909  stoweidlem7  37968  stoweidlem15  37976  stoweidlem35  37997  wallispilem3  38030  fourierdlem68  38139  fourierdlem71  38142  fourierdlem73  38144  fourierdlem87  38158  fourierdlem100  38171  fourierdlem103  38174  fourierdlem104  38175  fourierdlem107  38178  fourierdlem109  38180  fourierdlem112  38183  etransc  38250  qndenserrnbllem  38264  dfsalgen2  38301  ovnsubaddlem2  38500  hoidmvlelem5  38528  hoidmvle  38529  hoiqssbllem3  38553  bgoldbtbndlem4  39038  bgoldbtbnd  39039  nn0sumshdiglem1  40801
  Copyright terms: Public domain W3C validator