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

Theorem cbvralv 3308
Description: Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)
Hypothesis
Ref Expression
cbvralv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvralv (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvralv
StepHypRef Expression
1 nfv 1990 . 2 𝑦𝜑
2 nfv 1990 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvral 3304 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wral 3048
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clel 2754  df-nfc 2889  df-ral 3053
This theorem is referenced by:  cbvral2v  3316  cbvral3v  3318  reu7  3540  disjxun  4800  reusv3i  5022  wereu2  5261  cnvpo  5832  f1mpt  6679  grprinvlem  7035  grprinvd  7036  dfwe2  7144  tfinds  7222  wfrlem1  7581  tfrlem1  7639  tfrlem12  7652  rdglem1  7678  tz7.48lem  7703  nneneq  8306  marypha1lem  8502  supub  8528  suplub  8529  ordtypecbv  8585  ordtypelem3  8588  ordtypelem9  8594  wemaplem1  8614  brwdom3  8650  tcrank  8918  infxpenc2  9033  aceq1  9128  aceq2  9130  dfac5  9139  dfac9  9148  dfac12lem3  9157  kmlem12  9173  kmlem14  9175  cofsmo  9281  infpssrlem4  9318  isfin3ds  9341  isf32lem2  9366  isf32lem11  9375  isf33lem  9378  domtriomlem  9454  axdc3  9466  zorn2lem7  9514  zorn2g  9515  fpwwe2cbv  9642  fpwwecbv  9656  pwfseq  9676  axgroth6  9840  dedekind  10390  suprleub  11179  infregelb  11197  nnsub  11249  uzwo  11942  ublbneg  11964  zsupss  11968  xrub  12333  fsuppmapnn0fiubex  12984  monoord2  13024  faclbnd4lem4  13275  bccl  13301  hashbc  13427  wrdind  13674  wrd2ind  13675  reuccats1  13678  cau3lem  14291  climmpt2  14501  caucvgrlem  14600  caurcvg2  14605  caucvgb  14607  fsum0diag2  14712  incexclem  14765  cvgrat  14812  mertenslem2  14814  mertens  14815  sqrt2irr  15176  gcdcllem1  15421  lcmfunsnlem1  15550  lcmfunsnlem2lem1  15551  prmind2  15598  prmpwdvds  15808  prmreclem5  15824  prmreclem6  15825  vdwlem7  15891  vdwlem10  15894  vdwlem13  15897  vdwnn  15902  ramcl  15933  isacs2  16513  catpropd  16568  gsumvalx  17469  mrcmndind  17565  issubg4  17812  isnsg2  17823  elnmz  17832  gsmsymgreqlem2  18049  psgnunilem5  18112  psgnunilem3  18114  efgsdm  18341  gsummptnn0fzfv  18582  pgpfac1lem5  18676  pgpfac1  18677  pgpfac  18681  ablfaclem3  18684  lbsextg  19362  evlslem2  19712  mpfind  19736  cply1mul  19864  mdetuni0  20627  m2cpminvid2lem  20759  mp2pm2mplem4  20814  chcoeffeqlem  20890  cayhamlem3  20892  elcls3  21087  isclo2  21092  neiptopnei  21136  tgcn  21256  subbascn  21258  txcmplem2  21645  kqfvima  21733  kqt0lem  21739  isr0  21740  r0cld  21741  regr1lem2  21743  fbun  21843  flftg  21999  fclsbas  22024  alexsubALTlem2  22051  alexsubALTlem4  22053  ptcmplem4  22058  tsmsxplem1  22155  tsmsxp  22157  ustuqtop  22249  utopsnneip  22251  prdsxmslem2  22533  isclmp  23095  iscau4  23275  caucfil  23279  iscmet3  23289  bcthlem5  23323  bcth  23324  ovolicc2lem5  23487  uniioombllem6  23554  vitali  23579  ismbf3d  23618  itg1climres  23678  itg2seq  23706  itg2monolem1  23714  itg2mono  23717  rolle  23950  dvlipcn  23954  dvivthlem1  23968  ply1divex  24093  fta1g  24124  dgrco  24228  plydivex  24249  fta1  24260  vieta1  24264  ulmcaulem  24345  ulmcau  24346  abelthlem8  24390  wilth  24994  fta  25003  dchrelbas3  25160  2sqlem6  25345  2sqlem10  25350  dchrisumlem3  25377  dchrisum  25378  dchrmusumlema  25379  dchrvmasumlema  25386  dchrisum0lema  25400  pntibndlem3  25478  pntlem3  25495  pntleml  25497  pnt3  25498  ostth2lem2  25520  ostth  25525  axcontlem1  26041  axcontlem6  26046  uspgr2wlkeq  26750  crctcshwlkn0  26922  frgrwopreglem5ALT  27474  grpoideu  27670  ubthlem3  28035  adjsym  28999  lnopunilem1  29176  elunop2  29179  lnophm  29185  cnlnadjlem5  29237  mdbr3  29463  mdbr4  29464  dmdbr3  29471  dmdbr4  29472  mddmd2  29475  fprodex01  29878  toslublem  29974  tosglblem  29976  archiabl  30059  isarchiofld  30124  qtophaus  30210  lmdvg  30306  prodindf  30392  esumcvg  30455  unelldsys  30528  ldgenpisyslem1  30533  eulerpartlemsv3  30730  eulerpartlemgvv  30745  signstfvneq0  30956  reprinfz1  31007  tgoldbachgtd  31047  bnj1185  31169  bnj1379  31206  bnj222  31258  bnj517  31260  bnj1450  31423  bnj1452  31425  bnj1463  31428  derangenlem  31458  subfacp1lem6  31472  subfacp1  31473  resconn  31533  cvmscbv  31545  untangtr  31896  dfon2lem3  31993  dfon2lem7  31997  frpomin  32042  frrlem1  32084  nosupdm  32154  nosupbnd1lem4  32161  nosupbnd2  32166  nn0prpwlem  32621  neibastop3  32661  fnemeet2  32666  phpreu  33704  poimirlem27  33747  heicant  33755  mblfinlem2  33758  ovoliunnfl  33762  voliunnfl  33764  mbfresfi  33767  upixp  33835  sdclem2  33849  fdc  33852  mettrifi  33864  heiborlem5  33925  heiborlem10  33930  heibor  33931  bfp  33934  cdleme25cv  36146  cdleme40v  36257  mzpclval  37788  dford3lem1  38093  fnwe2lem1  38120  aomclem3  38126  aomclem4  38127  aomclem8  38131  dfac11  38132  hbtlem5  38198  ntrk2imkb  38835  ntrclsk2  38866  ntrclsk4  38870  fnchoice  39685  cncmpmax  39688  wessf1ornlem  39868  disjinfi  39877  rnmptbdd  39953  rnmptbd2  39961  rnmptbd  39968  supxrunb3  40119  unb2ltle  40138  monoord2xrv  40210  uzubioo2  40297  mccl  40331  climsuse  40341  limsupre  40374  limsuppnfd  40435  limsuppnf  40444  limsupubuz  40446  limsupmnf  40454  limsupre2  40458  limsupmnfuz  40460  limsupre2mpt  40463  limsupre3  40466  limsupre3mpt  40467  limsupre3uzlem  40468  limsupre3uz  40469  limsupreuz  40470  limsupvaluz2  40471  limsupreuzmpt  40472  climuz  40477  lmbr3  40480  limsupge  40494  liminfreuz  40536  cnrefiisp  40557  xlimmnf  40568  xlimpnf  40569  xlimmnfmpt  40570  xlimpnfmpt  40571  dfxlim2  40575  dvbdfbdioolem2  40645  dvbdfbdioo  40646  ioodvbdlimc1lem1  40647  ioodvbdlimc1lem2  40648  ioodvbdlimc2lem  40650  dvnprodlem3  40664  stoweidlem7  40725  stoweidlem15  40733  stoweidlem35  40753  wallispilem3  40785  fourierdlem68  40892  fourierdlem71  40895  fourierdlem73  40897  fourierdlem87  40911  fourierdlem100  40924  fourierdlem103  40927  fourierdlem104  40928  fourierdlem107  40931  fourierdlem109  40933  fourierdlem112  40936  etransc  41001  qndenserrnbllem  41015  dfsalgen2  41060  subsaliuncl  41077  meaiuninclem  41198  ovnsubaddlem2  41289  hoidmvlelem5  41317  hoidmvle  41318  hoiqssbllem3  41342  vonioo  41400  vonicc  41403  issmf  41441  issmfle  41458  issmfgt  41469  issmfge  41482  smfsuplem2  41522  sbgoldbm  42180  mogoldbb  42181  bgoldbtbndlem4  42204  bgoldbtbnd  42205  nn0sumshdiglem1  42923
  Copyright terms: Public domain W3C validator