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

Theorem cbvralv 3070
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 1694 . 2  |-  F/ y
ph
2 nfv 1694 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 3066 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1600  df-nf 1604  df-sb 1727  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798
This theorem is referenced by:  cbvral2v  3078  cbvral3v  3080  reu7  3280  disjxun  4435  reusv3i  4644  wereu2  4866  cnvpo  5535  f1mpt  6154  grprinvlem  6498  grprinvd  6499  dfwe2  6602  tfinds  6679  tfrlem1  7047  tfrlem12  7060  rdglem1  7083  tz7.48lem  7108  nneneq  7702  marypha1lem  7895  supub  7921  suplub  7922  supmaxlemOLD  7927  ordtypecbv  7945  ordtypelem3  7948  ordtypelem9  7954  wemaplem1  7974  brwdom3  8011  tcrank  8305  infxpenc2  8402  infxpenc2OLD  8406  aceq1  8501  aceq2  8503  dfac5  8512  dfac9  8519  dfac12lem3  8528  kmlem12  8544  kmlem14  8546  cofsmo  8652  infpssrlem4  8689  isfin3ds  8712  isf32lem2  8737  isf32lem11  8746  isf33lem  8749  domtriomlem  8825  axdc3  8837  zorn2lem7  8885  zorn2g  8886  fpwwe2cbv  9011  fpwwecbv  9025  pwfseq  9045  axgroth6  9209  dedekind  9747  suprleub  10514  infmrgelb  10530  nnsub  10581  uzwo  11154  uzwoOLD  11155  ublbneg  11176  zsupss  11181  xrub  11513  fsuppmapnn0fiubex  12079  monoord2  12119  faclbnd4lem4  12355  bccl  12381  hashbc  12483  wrdind  12683  wrd2ind  12684  reuccats1  12687  cau3lem  13168  climmpt2  13377  caucvgrlem  13476  caurcvg2  13481  caucvgb  13483  fsum0diag2  13579  incexclem  13629  cvgrat  13673  mertenslem2  13675  mertens  13676  sqrt2irr  13963  gcdcllem1  14130  prmind2  14209  prmpwdvds  14403  prmreclem5  14419  prmreclem6  14420  vdwlem7  14486  vdwlem10  14489  vdwlem13  14492  vdwnn  14497  ramcl  14528  isacs2  15031  catpropd  15085  gsumvalx  15875  mrcmndind  15975  issubg4  16198  isnsg2  16209  elnmz  16218  gsmsymgreqlem2  16434  psgnunilem5  16497  psgnunilem3  16499  efgsdm  16726  gsummptnn0fzfv  16994  pgpfac1lem5  17108  pgpfac1  17109  pgpfac  17113  ablfaclem3  17116  lbsextg  17786  evlslem2  18158  mpfind  18183  cply1mul  18313  mdetuni0  19100  m2cpminvid2lem  19232  mp2pm2mplem4  19287  chcoeffeqlem  19363  cayhamlem3  19365  elcls3  19561  isclo2  19566  neiptopnei  19610  tgcn  19730  subbascn  19732  txcmplem2  20120  kqfvima  20208  kqt0lem  20214  isr0  20215  r0cld  20216  regr1lem2  20218  fbun  20318  flftg  20474  fclsbas  20499  alexsubALTlem2  20525  alexsubALTlem4  20527  ptcmplem4  20532  tsmsxplem1  20632  tsmsxp  20634  ustuqtop  20726  utopsnneip  20728  prdsxmslem2  21009  iscau4  21695  caucfil  21699  iscmet3  21709  bcthlem5  21744  bcth  21745  ovolicc2lem5  21909  uniioombllem6  21974  vitali  21999  ismbf3d  22038  itg1climres  22098  itg2seq  22126  itg2monolem1  22134  itg2mono  22137  rolle  22368  dvlipcn  22372  dvivthlem1  22386  ply1divex  22514  fta1g  22545  dgrco  22648  plydivex  22669  fta1  22680  vieta1  22684  ulmcaulem  22765  ulmcau  22766  abelthlem8  22810  wilth  23321  fta  23329  dchrelbas3  23489  2sqlem6  23620  2sqlem10  23625  dchrisumlem3  23652  dchrisum  23653  dchrmusumlema  23654  dchrvmasumlema  23661  dchrisum0lema  23675  pntibndlem3  23753  pntlem3  23770  pntleml  23772  pnt3  23773  ostth2lem2  23795  ostth  23800  axcontlem1  24243  axcontlem6  24248  cusgrafilem2  24456  usg2wlkeq  24684  grpoideu  25187  ubthlem3  25764  adjsym  26728  lnopunilem1  26905  elunop2  26908  lnophm  26914  cnlnadjlem5  26966  mdbr3  27192  mdbr4  27193  dmdbr3  27200  dmdbr4  27201  mddmd2  27204  toslublem  27632  tosglblem  27634  archiabl  27719  isarchiofld  27784  qtophaus  27816  lmdvg  27912  esumcvg  28069  eulerpartlemsv3  28277  eulerpartlemgvv  28292  signstfvneq0  28506  derangenlem  28592  subfacp1lem6  28606  subfacp1  28607  rescon  28668  cvmscbv  28680  untangtr  29063  dfon2lem3  29192  dfon2lem7  29196  cbvsetlike  29236  wfrlem1  29318  frrlem1  29362  heicant  30024  mblfinlem2  30027  ovoliunnfl  30031  voliunnfl  30033  mbfresfi  30036  nn0prpwlem  30115  neibastop3  30155  fnemeet2  30160  upixp  30195  sdclem2  30210  fdc  30213  mettrifi  30225  heiborlem5  30286  heiborlem10  30291  heibor  30292  bfp  30295  mzpclval  30632  dford3lem1  30943  fnwe2lem1  30971  aomclem3  30977  aomclem4  30978  aomclem8  30982  dfac11  30983  hbtlem5  31052  fnchoice  31358  cncmpmax  31361  climsuse  31522  limsupre  31555  dvbdfbdioolem2  31630  dvbdfbdioo  31631  ioodvbdlimc1lem1  31632  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  stoweidlem7  31678  stoweidlem15  31686  stoweidlem35  31706  wallispilem3  31738  fourierdlem68  31846  fourierdlem71  31849  fourierdlem73  31851  fourierdlem87  31865  fourierdlem100  31878  fourierdlem103  31881  fourierdlem104  31882  fourierdlem107  31885  fourierdlem109  31887  fourierdlem112  31890  bnj1185  33585  bnj1379  33622  bnj222  33674  bnj517  33676  bnj1450  33839  bnj1452  33841  bnj1463  33844  cdleme25cv  35824  cdleme40v  35935
  Copyright terms: Public domain W3C validator