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

Theorem cbvralv 3371
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 2005 . 2 𝑦𝜑
2 nfv 2005 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvral 3367 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wral 3107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clel 2813  df-nfc 2948  df-ral 3112
This theorem is referenced by:  cbvral2v  3379  cbvral3v  3381  reu7  3610  disjxun  4853  reusv3i  5086  wereu2  5321  cnvpo  5901  f1mpt  6752  grprinvlem  7112  grprinvd  7113  dfwe2  7221  tfinds  7299  wfrlem1  7659  tfrlem1  7718  tfrlem12  7731  rdglem1  7757  tz7.48lem  7782  nneneq  8392  marypha1lem  8588  supub  8614  suplub  8615  ordtypecbv  8671  ordtypelem3  8674  ordtypelem9  8680  wemaplem1  8700  brwdom3  8736  tcrank  9004  infxpenc2  9138  aceq1  9233  aceq2  9235  dfac5  9244  dfac9  9253  dfac12lem3  9262  kmlem12  9278  kmlem14  9280  cofsmo  9386  infpssrlem4  9423  isfin3ds  9446  isf32lem2  9471  isf32lem11  9480  isf33lem  9483  domtriomlem  9559  axdc3  9571  zorn2lem7  9619  zorn2g  9620  fpwwe2cbv  9747  fpwwecbv  9761  pwfseq  9781  axgroth6  9945  dedekind  10495  suprleub  11284  infregelb  11302  nnsub  11357  uzwo  11990  ublbneg  12012  zsupss  12016  xrub  12380  fsuppmapnn0fiubex  13035  monoord2  13075  faclbnd4lem4  13323  bccl  13349  hashbc  13474  wrdind  13720  wrd2ind  13721  reuccats1  13724  cau3lem  14337  climmpt2  14547  caucvgrlem  14646  caurcvg2  14651  caucvgb  14653  fsum0diag2  14757  incexclem  14810  cvgrat  14856  mertenslem2  14858  mertens  14859  sqrt2irr  15219  gcdcllem1  15460  lcmfunsnlem1  15589  lcmfunsnlem2lem1  15590  prmind2  15636  prmpwdvds  15845  prmreclem5  15861  prmreclem6  15862  vdwlem7  15928  vdwlem10  15931  vdwlem13  15934  vdwnn  15939  ramcl  15970  isacs2  16538  catpropd  16593  gsumvalx  17495  mrcmndind  17591  issubg4  17835  isnsg2  17846  elnmz  17855  gsmsymgreqlem2  18072  psgnunilem5  18135  psgnunilem3  18137  efgsdm  18364  gsummptnn0fzfv  18606  pgpfac1lem5  18700  pgpfac1  18701  pgpfac  18705  ablfaclem3  18708  lbsextg  19391  evlslem2  19740  mpfind  19764  cply1mul  19892  mdetuni0  20659  m2cpminvid2lem  20793  mp2pm2mplem4  20848  chcoeffeqlem  20924  cayhamlem3  20926  elcls3  21122  isclo2  21127  neiptopnei  21171  tgcn  21291  subbascn  21293  txcmplem2  21680  kqfvima  21768  kqt0lem  21774  isr0  21775  r0cld  21776  regr1lem2  21778  fbun  21878  flftg  22034  fclsbas  22059  alexsubALTlem2  22086  alexsubALTlem4  22088  ptcmplem4  22093  tsmsxplem1  22190  tsmsxp  22192  ustuqtop  22284  utopsnneip  22286  prdsxmslem2  22568  isclmp  23130  iscau4  23311  caucfil  23315  iscmet3  23325  bcthlem5  23359  bcth  23360  ovolicc2lem5  23525  uniioombllem6  23592  vitali  23617  ismbf3d  23658  itg1climres  23718  itg2seq  23746  itg2monolem1  23754  itg2mono  23757  rolle  23990  dvlipcn  23994  dvivthlem1  24008  ply1divex  24133  fta1g  24164  dgrco  24268  plydivex  24289  fta1  24300  vieta1  24304  ulmcaulem  24385  ulmcau  24386  abelthlem8  24430  wilth  25034  fta  25043  dchrelbas3  25200  2sqlem6  25385  2sqlem10  25390  dchrisumlem3  25417  dchrisum  25418  dchrmusumlema  25419  dchrvmasumlema  25426  dchrisum0lema  25440  pntibndlem3  25518  pntlem3  25535  pntleml  25537  pnt3  25538  ostth2lem2  25560  ostth  25565  axcontlem1  26081  axcontlem6  26086  uspgr2wlkeq  26793  crctcshwlkn0  26965  frgrwopreglem5ALT  27520  grpoideu  27715  ubthlem3  28079  adjsym  29043  lnopunilem1  29220  elunop2  29223  lnophm  29229  cnlnadjlem5  29281  mdbr3  29507  mdbr4  29508  dmdbr3  29515  dmdbr4  29516  mddmd2  29519  fprodex01  29921  toslublem  30015  tosglblem  30017  archiabl  30100  isarchiofld  30165  qtophaus  30251  lmdvg  30347  prodindf  30433  esumcvg  30496  unelldsys  30569  ldgenpisyslem1  30574  eulerpartlemsv3  30771  eulerpartlemgvv  30786  signstfvneq0  30997  reprinfz1  31048  tgoldbachgtd  31088  bnj1185  31209  bnj1379  31246  bnj222  31298  bnj517  31300  bnj1450  31463  bnj1452  31465  bnj1463  31468  derangenlem  31498  subfacp1lem6  31512  subfacp1  31513  resconn  31573  cvmscbv  31585  untangtr  31935  dfon2lem3  32032  dfon2lem7  32036  frpomin  32081  frrlem1  32123  nosupdm  32193  nosupbnd1lem4  32200  nosupbnd2  32205  nn0prpwlem  32660  neibastop3  32700  fnemeet2  32705  phpreu  33725  poimirlem27  33768  heicant  33776  mblfinlem2  33779  ovoliunnfl  33783  voliunnfl  33785  mbfresfi  33787  upixp  33855  sdclem2  33868  fdc  33871  mettrifi  33883  heiborlem5  33944  heiborlem10  33949  heibor  33950  bfp  33953  cdleme25cv  36157  cdleme40v  36268  mzpclval  37808  dford3lem1  38112  fnwe2lem1  38139  aomclem3  38145  aomclem4  38146  aomclem8  38150  dfac11  38151  hbtlem5  38217  ntrk2imkb  38853  ntrclsk2  38884  ntrclsk4  38888  fnchoice  39700  cncmpmax  39703  wessf1ornlem  39878  disjinfi  39887  rnmptbdd  39958  rnmptbd2  39965  rnmptbd  39972  supxrunb3  40120  unb2ltle  40139  monoord2xrv  40211  uzubioo2  40294  mccl  40328  climsuse  40338  limsupre  40371  limsuppnfd  40432  limsuppnf  40441  limsupubuz  40443  limsupmnf  40451  limsupre2  40455  limsupmnfuz  40457  limsupre2mpt  40460  limsupre3  40463  limsupre3mpt  40464  limsupre3uzlem  40465  limsupre3uz  40466  limsupreuz  40467  limsupvaluz2  40468  limsupreuzmpt  40469  climuz  40474  lmbr3  40477  limsupge  40491  liminfreuz  40533  cnrefiisp  40554  xlimmnf  40565  xlimpnf  40566  xlimmnfmpt  40567  xlimpnfmpt  40568  dfxlim2  40572  dvbdfbdioolem2  40642  dvbdfbdioo  40643  ioodvbdlimc1lem1  40644  ioodvbdlimc1lem2  40645  ioodvbdlimc2lem  40647  dvnprodlem3  40661  stoweidlem7  40721  stoweidlem15  40729  stoweidlem35  40749  wallispilem3  40781  fourierdlem68  40888  fourierdlem71  40891  fourierdlem73  40893  fourierdlem87  40907  fourierdlem100  40920  fourierdlem103  40923  fourierdlem104  40924  fourierdlem107  40927  fourierdlem109  40929  fourierdlem112  40932  etransc  40997  qndenserrnbllem  41011  dfsalgen2  41056  subsaliuncl  41073  meaiuninclem  41194  ovnsubaddlem2  41285  hoidmvlelem5  41313  hoidmvle  41314  hoiqssbllem3  41338  vonioo  41396  vonicc  41399  issmf  41437  issmfle  41454  issmfgt  41465  issmfge  41478  smfsuplem2  41518  sbgoldbm  42265  mogoldbb  42266  bgoldbtbndlem4  42289  bgoldbtbnd  42290  nn0sumshdiglem1  43001
  Copyright terms: Public domain W3C validator