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

Theorem cbvralv 3163
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 1840 . 2 𝑦𝜑
2 nfv 1840 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvral 3159 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913
This theorem is referenced by:  cbvral2v  3171  cbvral3v  3173  reu7  3388  disjxun  4621  reusv3i  4845  wereu2  5081  cnvpo  5642  f1mpt  6483  grprinvlem  6837  grprinvd  6838  dfwe2  6943  tfinds  7021  wfrlem1  7374  tfrlem1  7432  tfrlem12  7445  rdglem1  7471  tz7.48lem  7496  nneneq  8103  marypha1lem  8299  supub  8325  suplub  8326  ordtypecbv  8382  ordtypelem3  8385  ordtypelem9  8391  wemaplem1  8411  brwdom3  8447  tcrank  8707  infxpenc2  8805  aceq1  8900  aceq2  8902  dfac5  8911  dfac9  8918  dfac12lem3  8927  kmlem12  8943  kmlem14  8945  cofsmo  9051  infpssrlem4  9088  isfin3ds  9111  isf32lem2  9136  isf32lem11  9145  isf33lem  9148  domtriomlem  9224  axdc3  9236  zorn2lem7  9284  zorn2g  9285  fpwwe2cbv  9412  fpwwecbv  9426  pwfseq  9446  axgroth6  9610  dedekind  10160  suprleub  10949  infregelb  10967  nnsub  11019  uzwo  11711  ublbneg  11733  zsupss  11737  xrub  12101  fsuppmapnn0fiubex  12748  monoord2  12788  faclbnd4lem4  13039  bccl  13065  hashbc  13191  wrdind  13430  wrd2ind  13431  reuccats1  13434  cau3lem  14044  climmpt2  14254  caucvgrlem  14353  caurcvg2  14358  caucvgb  14360  fsum0diag2  14462  incexclem  14512  cvgrat  14559  mertenslem2  14561  mertens  14562  sqrt2irr  14922  gcdcllem1  15164  lcmfunsnlem1  15293  lcmfunsnlem2lem1  15294  prmind2  15341  prmpwdvds  15551  prmreclem5  15567  prmreclem6  15568  vdwlem7  15634  vdwlem10  15637  vdwlem13  15640  vdwnn  15645  ramcl  15676  isacs2  16254  catpropd  16309  gsumvalx  17210  mrcmndind  17306  issubg4  17553  isnsg2  17564  elnmz  17573  gsmsymgreqlem2  17791  psgnunilem5  17854  psgnunilem3  17856  efgsdm  18083  gsummptnn0fzfv  18324  pgpfac1lem5  18418  pgpfac1  18419  pgpfac  18423  ablfaclem3  18426  lbsextg  19102  evlslem2  19452  mpfind  19476  cply1mul  19604  mdetuni0  20367  m2cpminvid2lem  20499  mp2pm2mplem4  20554  chcoeffeqlem  20630  cayhamlem3  20632  elcls3  20827  isclo2  20832  neiptopnei  20876  tgcn  20996  subbascn  20998  txcmplem2  21385  kqfvima  21473  kqt0lem  21479  isr0  21480  r0cld  21481  regr1lem2  21483  fbun  21584  flftg  21740  fclsbas  21765  alexsubALTlem2  21792  alexsubALTlem4  21794  ptcmplem4  21799  tsmsxplem1  21896  tsmsxp  21898  ustuqtop  21990  utopsnneip  21992  prdsxmslem2  22274  isclmp  22837  iscau4  23017  caucfil  23021  iscmet3  23031  bcthlem5  23065  bcth  23066  ovolicc2lem5  23229  uniioombllem6  23296  vitali  23322  ismbf3d  23361  itg1climres  23421  itg2seq  23449  itg2monolem1  23457  itg2mono  23460  rolle  23691  dvlipcn  23695  dvivthlem1  23709  ply1divex  23834  fta1g  23865  dgrco  23969  plydivex  23990  fta1  24001  vieta1  24005  ulmcaulem  24086  ulmcau  24087  abelthlem8  24131  wilth  24731  fta  24740  dchrelbas3  24897  2sqlem6  25082  2sqlem10  25087  dchrisumlem3  25114  dchrisum  25115  dchrmusumlema  25116  dchrvmasumlema  25123  dchrisum0lema  25137  pntibndlem3  25215  pntlem3  25232  pntleml  25234  pnt3  25235  ostth2lem2  25257  ostth  25262  axcontlem1  25778  axcontlem6  25783  uspgr2wlkeq  26445  crctcshwlkn0  26616  grpoideu  27251  ubthlem3  27616  adjsym  28580  lnopunilem1  28757  elunop2  28760  lnophm  28766  cnlnadjlem5  28818  mdbr3  29044  mdbr4  29045  dmdbr3  29052  dmdbr4  29053  mddmd2  29056  toslublem  29494  tosglblem  29496  archiabl  29579  isarchiofld  29644  qtophaus  29727  lmdvg  29823  esumcvg  29971  unelldsys  30044  ldgenpisyslem1  30049  eulerpartlemsv3  30246  eulerpartlemgvv  30261  signstfvneq0  30471  bnj1185  30625  bnj1379  30662  bnj222  30714  bnj517  30716  bnj1450  30879  bnj1452  30881  bnj1463  30884  derangenlem  30914  subfacp1lem6  30928  subfacp1  30929  resconn  30989  cvmscbv  31001  untangtr  31352  dfon2lem3  31444  dfon2lem7  31448  frrlem1  31534  nn0prpwlem  32012  neibastop3  32052  fnemeet2  32057  phpreu  33064  poimirlem27  33107  heicant  33115  mblfinlem2  33118  ovoliunnfl  33122  voliunnfl  33124  mbfresfi  33127  upixp  33195  sdclem2  33209  fdc  33212  mettrifi  33224  heiborlem5  33285  heiborlem10  33290  heibor  33291  bfp  33294  cdleme25cv  35165  cdleme40v  35276  mzpclval  36807  dford3lem1  37112  fnwe2lem1  37139  aomclem3  37145  aomclem4  37146  aomclem8  37150  dfac11  37151  hbtlem5  37218  ntrk2imkb  37856  ntrclsk2  37887  ntrclsk4  37891  fnchoice  38710  cncmpmax  38713  wessf1ornlem  38880  disjinfi  38889  rnmptbdd  38966  rnmptbd2  38975  rnmptbd  38982  supxrunb3  39122  unb2ltle  39141  mccl  39266  climsuse  39276  limsupre  39309  limsuppnfd  39370  limsuppnf  39379  limsupubuz  39381  limsupmnf  39389  limsupre2  39393  limsupmnfuz  39395  limsupre2mpt  39398  limsupre3  39401  limsupre3mpt  39402  limsupre3uzlem  39403  limsupre3uz  39404  limsupreuz  39405  limsupvaluz2  39406  limsupreuzmpt  39407  dvbdfbdioolem2  39481  dvbdfbdioo  39482  ioodvbdlimc1lem1  39483  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvnprodlem3  39500  stoweidlem7  39561  stoweidlem15  39569  stoweidlem35  39589  wallispilem3  39621  fourierdlem68  39728  fourierdlem71  39731  fourierdlem73  39733  fourierdlem87  39747  fourierdlem100  39760  fourierdlem103  39763  fourierdlem104  39764  fourierdlem107  39767  fourierdlem109  39769  fourierdlem112  39772  etransc  39837  qndenserrnbllem  39851  dfsalgen2  39896  subsaliuncl  39913  meaiuninclem  40034  ovnsubaddlem2  40122  hoidmvlelem5  40150  hoidmvle  40151  hoiqssbllem3  40175  vonioo  40233  vonicc  40236  issmf  40274  issmfle  40291  issmfgt  40302  issmfge  40315  smfsuplem2  40355  bgoldbtbndlem4  41015  bgoldbtbnd  41016  nn0sumshdiglem1  41737
  Copyright terms: Public domain W3C validator