ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cbvralv Unicode version

Theorem cbvralv 2590
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 1466 . 2  |-  F/ y
ph
2 nfv 1466 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2586 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   A.wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364
This theorem is referenced by:  cbvral2v  2598  cbvral3v  2600  reu7  2808  reusv3i  4272  omsinds  4425  cnvpom  4960  f1mpt  5532  grprinvlem  5821  grprinvd  5822  tfrlem1  6055  tfrlemiubacc  6077  tfrlemi1  6079  tfr1onlemubacc  6093  tfr1onlemaccex  6095  tfrcllembxssdm  6103  tfrcllemubacc  6106  tfrcllemaccex  6108  tfrcllemres  6109  tfrcldm  6110  rdgon  6133  frecfcllem  6151  frecsuclem  6153  nneneq  6553  fimax2gtrilemstep  6596  supubti  6673  suplubti  6674  finomni  6775  cauappcvgprlemladdrl  7195  caucvgprlemcl  7214  caucvgprlemladdrl  7216  caucvgsrlembound  7318  caucvgsrlemgt1  7319  caucvgsrlemoffres  7324  peano5nnnn  7406  axcaucvglemres  7413  suprleubex  8387  nnsub  8432  supinfneg  9052  infsupneg  9053  ublbneg  9067  exbtwnzlemex  9626  uzsinds  9813  iseqovex  9835  iseqval  9836  iseqvalt  9838  seq3val  9839  iseqfclt  9844  seqf  9845  monoord2  9870  iseqf1olemjpcl  9889  iseqf1olemqpcl  9890  seq3f1olemqsum  9894  seq3f1olemp  9896  seq3f1oleml  9897  seq3f1o  9898  bccl  10140  seq3shft  10237  caucvgre  10379  cvg1nlemcau  10382  resqrexlemglsq  10420  resqrexlemsqa  10422  resqrexlemex  10423  cau3lem  10512  zisum  10738  fisum  10742  isumz  10745  isumss2  10749  fisumsers  10751  fisumser  10753  fisum0diag2  10804  bezoutlemmain  11069  bezoutlemex  11072  bezoutlemzz  11073  bezoutlemeu  11078  bezoutlemle  11079  dfgcd3  11081  prmind2  11184  sqrt2irr  11223  hashdvds  11279  nnsf  11541  nninfsellemqall  11553  nninfomni  11557
  Copyright terms: Public domain W3C validator