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

Theorem cbvralv 2550
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 1437 . 2  |-  F/ y
ph
2 nfv 1437 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvral 2546 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102   A.wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328
This theorem is referenced by:  cbvral2v  2558  cbvral3v  2560  reu7  2759  reusv3i  4219  cnvpom  4888  f1mpt  5438  grprinvlem  5723  grprinvd  5724  tfrlem1  5954  tfrlemiubacc  5975  tfrlemi1  5977  rdgon  6004  nneneq  6351  supubti  6405  suplubti  6406  cauappcvgprlemladdrl  6813  caucvgprlemcl  6832  caucvgprlemladdrl  6834  caucvgsrlembound  6936  caucvgsrlemgt1  6937  caucvgsrlemoffres  6942  peano5nnnn  7024  axcaucvglemres  7031  nnsub  8028  ublbneg  8645  iseqovex  9383  iseqval  9384  monoord2  9400  bccl  9635  caucvgre  9808  cvg1nlemcau  9811  resqrexlemglsq  9849  resqrexlemsqa  9851  resqrexlemex  9852  cau3lem  9941  sqrt2irr  10251
  Copyright terms: Public domain W3C validator