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

Theorem cbvralv 3201
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 1883 . 2 𝑦𝜑
2 nfv 1883 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvral 3197 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946
This theorem is referenced by:  cbvral2v  3209  cbvral3v  3211  reu7  3434  disjxun  4683  reusv3i  4905  wereu2  5140  cnvpo  5711  f1mpt  6558  grprinvlem  6914  grprinvd  6915  dfwe2  7023  tfinds  7101  wfrlem1  7459  tfrlem1  7517  tfrlem12  7530  rdglem1  7556  tz7.48lem  7581  nneneq  8184  marypha1lem  8380  supub  8406  suplub  8407  ordtypecbv  8463  ordtypelem3  8466  ordtypelem9  8472  wemaplem1  8492  brwdom3  8528  tcrank  8785  infxpenc2  8883  aceq1  8978  aceq2  8980  dfac5  8989  dfac9  8996  dfac12lem3  9005  kmlem12  9021  kmlem14  9023  cofsmo  9129  infpssrlem4  9166  isfin3ds  9189  isf32lem2  9214  isf32lem11  9223  isf33lem  9226  domtriomlem  9302  axdc3  9314  zorn2lem7  9362  zorn2g  9363  fpwwe2cbv  9490  fpwwecbv  9504  pwfseq  9524  axgroth6  9688  dedekind  10238  suprleub  11027  infregelb  11045  nnsub  11097  uzwo  11789  ublbneg  11811  zsupss  11815  xrub  12180  fsuppmapnn0fiubex  12832  monoord2  12872  faclbnd4lem4  13123  bccl  13149  hashbc  13275  wrdind  13522  wrd2ind  13523  reuccats1  13526  cau3lem  14138  climmpt2  14348  caucvgrlem  14447  caurcvg2  14452  caucvgb  14454  fsum0diag2  14559  incexclem  14612  cvgrat  14659  mertenslem2  14661  mertens  14662  sqrt2irr  15023  gcdcllem1  15268  lcmfunsnlem1  15397  lcmfunsnlem2lem1  15398  prmind2  15445  prmpwdvds  15655  prmreclem5  15671  prmreclem6  15672  vdwlem7  15738  vdwlem10  15741  vdwlem13  15744  vdwnn  15749  ramcl  15780  isacs2  16361  catpropd  16416  gsumvalx  17317  mrcmndind  17413  issubg4  17660  isnsg2  17671  elnmz  17680  gsmsymgreqlem2  17897  psgnunilem5  17960  psgnunilem3  17962  efgsdm  18189  gsummptnn0fzfv  18430  pgpfac1lem5  18524  pgpfac1  18525  pgpfac  18529  ablfaclem3  18532  lbsextg  19210  evlslem2  19560  mpfind  19584  cply1mul  19712  mdetuni0  20475  m2cpminvid2lem  20607  mp2pm2mplem4  20662  chcoeffeqlem  20738  cayhamlem3  20740  elcls3  20935  isclo2  20940  neiptopnei  20984  tgcn  21104  subbascn  21106  txcmplem2  21493  kqfvima  21581  kqt0lem  21587  isr0  21588  r0cld  21589  regr1lem2  21591  fbun  21691  flftg  21847  fclsbas  21872  alexsubALTlem2  21899  alexsubALTlem4  21901  ptcmplem4  21906  tsmsxplem1  22003  tsmsxp  22005  ustuqtop  22097  utopsnneip  22099  prdsxmslem2  22381  isclmp  22943  iscau4  23123  caucfil  23127  iscmet3  23137  bcthlem5  23171  bcth  23172  ovolicc2lem5  23335  uniioombllem6  23402  vitali  23427  ismbf3d  23466  itg1climres  23526  itg2seq  23554  itg2monolem1  23562  itg2mono  23565  rolle  23798  dvlipcn  23802  dvivthlem1  23816  ply1divex  23941  fta1g  23972  dgrco  24076  plydivex  24097  fta1  24108  vieta1  24112  ulmcaulem  24193  ulmcau  24194  abelthlem8  24238  wilth  24842  fta  24851  dchrelbas3  25008  2sqlem6  25193  2sqlem10  25198  dchrisumlem3  25225  dchrisum  25226  dchrmusumlema  25227  dchrvmasumlema  25234  dchrisum0lema  25248  pntibndlem3  25326  pntlem3  25343  pntleml  25345  pnt3  25346  ostth2lem2  25368  ostth  25373  axcontlem1  25889  axcontlem6  25894  uspgr2wlkeq  26598  crctcshwlkn0  26769  frgrwopreglem5ALT  27302  grpoideu  27491  ubthlem3  27856  adjsym  28820  lnopunilem1  28997  elunop2  29000  lnophm  29006  cnlnadjlem5  29058  mdbr3  29284  mdbr4  29285  dmdbr3  29292  dmdbr4  29293  mddmd2  29296  fprodex01  29699  toslublem  29795  tosglblem  29797  archiabl  29880  isarchiofld  29945  qtophaus  30031  lmdvg  30127  prodindf  30213  esumcvg  30276  unelldsys  30349  ldgenpisyslem1  30354  eulerpartlemsv3  30551  eulerpartlemgvv  30566  signstfvneq0  30777  reprinfz1  30828  tgoldbachgtd  30868  bnj1185  30990  bnj1379  31027  bnj222  31079  bnj517  31081  bnj1450  31244  bnj1452  31246  bnj1463  31249  derangenlem  31279  subfacp1lem6  31293  subfacp1  31294  resconn  31354  cvmscbv  31366  untangtr  31717  dfon2lem3  31814  dfon2lem7  31818  frpomin  31863  frrlem1  31905  nosupdm  31975  nosupbnd1lem4  31982  nosupbnd2  31987  nn0prpwlem  32442  neibastop3  32482  fnemeet2  32487  phpreu  33523  poimirlem27  33566  heicant  33574  mblfinlem2  33577  ovoliunnfl  33581  voliunnfl  33583  mbfresfi  33586  upixp  33654  sdclem2  33668  fdc  33671  mettrifi  33683  heiborlem5  33744  heiborlem10  33749  heibor  33750  bfp  33753  cdleme25cv  35963  cdleme40v  36074  mzpclval  37605  dford3lem1  37910  fnwe2lem1  37937  aomclem3  37943  aomclem4  37944  aomclem8  37948  dfac11  37949  hbtlem5  38015  ntrk2imkb  38652  ntrclsk2  38683  ntrclsk4  38687  fnchoice  39502  cncmpmax  39505  wessf1ornlem  39685  disjinfi  39694  rnmptbdd  39770  rnmptbd2  39778  rnmptbd  39785  supxrunb3  39936  unb2ltle  39955  monoord2xrv  40027  uzubioo2  40114  mccl  40148  climsuse  40158  limsupre  40191  limsuppnfd  40252  limsuppnf  40261  limsupubuz  40263  limsupmnf  40271  limsupre2  40275  limsupmnfuz  40277  limsupre2mpt  40280  limsupre3  40283  limsupre3mpt  40284  limsupre3uzlem  40285  limsupre3uz  40286  limsupreuz  40287  limsupvaluz2  40288  limsupreuzmpt  40289  climuz  40294  lmbr3  40297  limsupge  40311  liminfreuz  40353  cnrefiisp  40374  xlimmnf  40385  xlimpnf  40386  xlimmnfmpt  40387  xlimpnfmpt  40388  dfxlim2  40392  dvbdfbdioolem2  40462  dvbdfbdioo  40463  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnprodlem3  40481  stoweidlem7  40542  stoweidlem15  40550  stoweidlem35  40570  wallispilem3  40602  fourierdlem68  40709  fourierdlem71  40712  fourierdlem73  40714  fourierdlem87  40728  fourierdlem100  40741  fourierdlem103  40744  fourierdlem104  40745  fourierdlem107  40748  fourierdlem109  40750  fourierdlem112  40753  etransc  40818  qndenserrnbllem  40832  dfsalgen2  40877  subsaliuncl  40894  meaiuninclem  41015  ovnsubaddlem2  41106  hoidmvlelem5  41134  hoidmvle  41135  hoiqssbllem3  41159  vonioo  41217  vonicc  41220  issmf  41258  issmfle  41275  issmfgt  41286  issmfge  41299  smfsuplem2  41339  sbgoldbm  41997  mogoldbb  41998  bgoldbtbndlem4  42021  bgoldbtbnd  42022  nn0sumshdiglem1  42740
  Copyright terms: Public domain W3C validator