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

Theorem cbvralv 2764
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 1605 . 2  |-  F/ y
ph
2 nfv 1605 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2760 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wral 2543
This theorem is referenced by:  cbvral2v  2772  cbvral3v  2774  reu7  2960  disjxun  4021  wereu2  4390  reusv3i  4541  dfwe2  4573  tfinds  4650  cnvpo  5213  f1mpt  5785  grprinvlem  6058  grprinvd  6059  tfrlem1  6391  tfrlem12  6405  rdglem1  6428  tz7.48lem  6453  nneneq  7044  marypha1lem  7186  supub  7210  suplub  7211  supmaxlem  7215  ordtypecbv  7232  ordtypelem3  7235  ordtypelem9  7241  wemaplem1  7261  brwdom3  7296  tcrank  7554  infxpenc2  7649  aceq1  7744  aceq2  7746  dfac5  7755  dfac9  7762  dfac12lem3  7771  kmlem12  7787  kmlem14  7789  cofsmo  7895  infpssrlem4  7932  isfin3ds  7955  isf32lem2  7980  isf32lem11  7989  isf33lem  7992  domtriomlem  8068  axdc3  8080  zorn2lem7  8129  zorn2g  8130  fpwwe2cbv  8252  fpwwecbv  8266  pwfseq  8286  axgroth6  8450  suprleub  9718  infmrgelb  9734  nnsub  9784  uzwo  10281  uzwoOLD  10282  ublbneg  10302  zsupss  10307  xrub  10630  monoord2  11077  faclbnd4lem4  11309  bccl  11334  hashbc  11391  wrdind  11477  cau3lem  11838  climmpt2  12047  caucvgrlem  12145  caurcvg2  12150  caucvgb  12152  fsum0diag2  12245  incexclem  12295  cvgrat  12339  mertenslem2  12341  mertens  12342  sqr2irr  12527  gcdcllem1  12690  prmind2  12769  prmpwdvds  12951  prmreclem5  12967  prmreclem6  12968  vdwlem7  13034  vdwlem10  13037  vdwlem13  13040  vdwnn  13045  ramcl  13076  isacs2  13555  catpropd  13612  spwmo  14335  gsumvalx  14451  issubg4  14638  isnsg2  14647  elnmz  14656  efgsdm  15039  pgpfac1lem5  15314  pgpfac1  15315  pgpfac  15319  ablfaclem3  15322  lbsextg  15915  evlslem2  16249  elcls3  16820  isclo2  16825  tgcn  16982  subbascn  16984  txcmplem2  17336  kqfvima  17421  kqt0lem  17427  isr0  17428  r0cld  17429  regr1lem2  17431  fbun  17535  flftg  17691  fclsbas  17716  alexsubALTlem2  17742  alexsubALTlem4  17744  ptcmplem4  17749  tsmsxplem1  17835  tsmsxp  17837  prdsxmslem2  18075  iscau4  18705  caucfil  18709  iscmet3  18719  bcthlem5  18750  bcth  18751  ovolicc2lem5  18880  uniioombllem6  18943  vitali  18968  ismbf3d  19009  itg1climres  19069  itg2seq  19097  itg2monolem1  19105  itg2mono  19108  rolle  19337  dvlipcn  19341  dvivthlem1  19355  mpfind  19428  ply1divex  19522  fta1g  19553  dgrco  19656  plydivex  19677  fta1  19688  vieta1  19692  ulmcaulem  19771  ulmcau  19772  abelthlem8  19815  wilth  20309  fta  20317  dchrelbas3  20477  2sqlem6  20608  2sqlem10  20613  dchrisumlem3  20640  dchrisum  20641  dchrmusumlema  20642  dchrvmasumlema  20649  dchrisum0lema  20663  pntibndlem3  20741  pntlem3  20758  pntleml  20760  pnt3  20761  ostth2lem2  20783  ostth  20788  grpoideu  20876  ubthlem3  21451  adjsym  22413  lnopunilem1  22590  elunop2  22593  lnophm  22599  cnlnadjlem5  22651  mdbr3  22877  mdbr4  22878  dmdbr3  22885  dmdbr4  22886  mddmd2  22889  esumcvg  23454  derangenlem  23702  subfacp1lem6  23716  subfacp1  23717  rescon  23777  cvmscbv  23789  untangtr  24060  dedekind  24082  dfon2lem3  24141  dfon2lem7  24145  cbvsetlike  24181  wfrlem1  24256  tfr3ALT  24279  frrlem1  24281  axcontlem1  24592  axcontlem6  24597  bpolyval  24784  celsor  25111  nn0prpwlem  26238  neibastop3  26311  fnemeet2  26316  upixp  26403  sdclem2  26452  fdc  26455  mettrifi  26473  heiborlem5  26539  heiborlem10  26544  heibor  26545  bfp  26548  mzpclval  26803  dford3lem1  27119  fnwe2lem1  27147  aomclem3  27153  aomclem4  27154  aomclem8  27159  dfac11  27160  hbtlem5  27332  psgnunilem5  27417  psgnunilem3  27419  fnchoice  27700  cncmpmax  27703  stoweidlem35  27784  bnj1185  28826  bnj1379  28863  bnj222  28915  bnj517  28917  bnj1450  29080  bnj1452  29082  bnj1463  29085  cdleme25cv  30547  cdleme40v  30658
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548
  Copyright terms: Public domain W3C validator