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

Theorem cbvralv 2777
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 1609 . 2  |-  F/ y
ph
2 nfv 1609 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2773 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 2556
This theorem is referenced by:  cbvral2v  2785  cbvral3v  2787  reu7  2973  disjxun  4037  wereu2  4406  reusv3i  4557  dfwe2  4589  tfinds  4666  cnvpo  5229  f1mpt  5801  grprinvlem  6074  grprinvd  6075  tfrlem1  6407  tfrlem12  6421  rdglem1  6444  tz7.48lem  6469  nneneq  7060  marypha1lem  7202  supub  7226  suplub  7227  supmaxlem  7231  ordtypecbv  7248  ordtypelem3  7251  ordtypelem9  7257  wemaplem1  7277  brwdom3  7312  tcrank  7570  infxpenc2  7665  aceq1  7760  aceq2  7762  dfac5  7771  dfac9  7778  dfac12lem3  7787  kmlem12  7803  kmlem14  7805  cofsmo  7911  infpssrlem4  7948  isfin3ds  7971  isf32lem2  7996  isf32lem11  8005  isf33lem  8008  domtriomlem  8084  axdc3  8096  zorn2lem7  8145  zorn2g  8146  fpwwe2cbv  8268  fpwwecbv  8282  pwfseq  8302  axgroth6  8466  suprleub  9734  infmrgelb  9750  nnsub  9800  uzwo  10297  uzwoOLD  10298  ublbneg  10318  zsupss  10323  xrub  10646  monoord2  11093  faclbnd4lem4  11325  bccl  11350  hashbc  11407  wrdind  11493  cau3lem  11854  climmpt2  12063  caucvgrlem  12161  caurcvg2  12166  caucvgb  12168  fsum0diag2  12261  incexclem  12311  cvgrat  12355  mertenslem2  12357  mertens  12358  sqr2irr  12543  gcdcllem1  12706  prmind2  12785  prmpwdvds  12967  prmreclem5  12983  prmreclem6  12984  vdwlem7  13050  vdwlem10  13053  vdwlem13  13056  vdwnn  13061  ramcl  13092  isacs2  13571  catpropd  13628  spwmo  14351  gsumvalx  14467  issubg4  14654  isnsg2  14663  elnmz  14672  efgsdm  15055  pgpfac1lem5  15330  pgpfac1  15331  pgpfac  15335  ablfaclem3  15338  lbsextg  15931  evlslem2  16265  elcls3  16836  isclo2  16841  tgcn  16998  subbascn  17000  txcmplem2  17352  kqfvima  17437  kqt0lem  17443  isr0  17444  r0cld  17445  regr1lem2  17447  fbun  17551  flftg  17707  fclsbas  17732  alexsubALTlem2  17758  alexsubALTlem4  17760  ptcmplem4  17765  tsmsxplem1  17851  tsmsxp  17853  prdsxmslem2  18091  iscau4  18721  caucfil  18725  iscmet3  18735  bcthlem5  18766  bcth  18767  ovolicc2lem5  18896  uniioombllem6  18959  vitali  18984  ismbf3d  19025  itg1climres  19085  itg2seq  19113  itg2monolem1  19121  itg2mono  19124  rolle  19353  dvlipcn  19357  dvivthlem1  19371  mpfind  19444  ply1divex  19538  fta1g  19569  dgrco  19672  plydivex  19693  fta1  19704  vieta1  19708  ulmcaulem  19787  ulmcau  19788  abelthlem8  19831  wilth  20325  fta  20333  dchrelbas3  20493  2sqlem6  20624  2sqlem10  20629  dchrisumlem3  20656  dchrisum  20657  dchrmusumlema  20658  dchrvmasumlema  20665  dchrisum0lema  20679  pntibndlem3  20757  pntlem3  20774  pntleml  20776  pnt3  20777  ostth2lem2  20799  ostth  20804  grpoideu  20892  ubthlem3  21467  adjsym  22429  lnopunilem1  22606  elunop2  22609  lnophm  22615  cnlnadjlem5  22667  mdbr3  22893  mdbr4  22894  dmdbr3  22901  dmdbr4  22902  mddmd2  22905  esumcvg  23469  derangenlem  23717  subfacp1lem6  23731  subfacp1  23732  rescon  23792  cvmscbv  23804  untangtr  24075  dedekind  24097  dfon2lem3  24212  dfon2lem7  24216  cbvsetlike  24252  wfrlem1  24327  tfr3ALT  24350  frrlem1  24352  axcontlem1  24664  axcontlem6  24669  bpolyval  24856  ovoliunnfl  25001  celsor  25214  nn0prpwlem  26341  neibastop3  26414  fnemeet2  26419  upixp  26506  sdclem2  26555  fdc  26558  mettrifi  26576  heiborlem5  26642  heiborlem10  26647  heibor  26648  bfp  26651  mzpclval  26906  dford3lem1  27222  fnwe2lem1  27250  aomclem3  27256  aomclem4  27257  aomclem8  27262  dfac11  27263  hbtlem5  27435  psgnunilem5  27520  psgnunilem3  27522  fnchoice  27803  cncmpmax  27806  stoweidlem35  27887  bnj1185  29142  bnj1379  29179  bnj222  29231  bnj517  29233  bnj1450  29396  bnj1452  29398  bnj1463  29401  cdleme25cv  31169  cdleme40v  31280
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561
  Copyright terms: Public domain W3C validator