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

Theorem cbvrexv 2584
Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)
Hypothesis
Ref Expression
cbvralv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvrexv  |-  ( E. x  e.  A  ph  <->  E. 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 cbvrexv
StepHypRef Expression
1 nfv 1462 . 2  |-  F/ y
ph
2 nfv 1462 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 2580 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   E.wrex 2354
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 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359
This theorem is referenced by:  cbvrex2v  2592  reu7  2797  reusv3  4239  funcnvuni  5020  fun11iun  5200  fvelimab  5283  fliftfun  5489  grpridd  5750  tfr1onlemaccex  6019  tfrcllemsucaccv  6025  tfrcllembxssdm  6027  tfrcllemaccex  6032  tfrcldm  6034  frecsuc  6078  nnaordex  6189  supmoti  6502  suplub2ti  6510  cardval3ex  6590  prarloclemlo  6823  prarloclem3  6826  cauappcvgprlemdisj  6980  cauappcvgprlemladdru  6985  cauappcvgprlemladdrl  6986  cauappcvgpr  6991  caucvgprlemdisj  7003  caucvgprlemcl  7005  caucvgprlemladdfu  7006  caucvgprlemladdrl  7007  caucvgpr  7011  caucvgprprlemell  7014  caucvgprprlemelu  7015  caucvgprprlemlol  7027  caucvgprprlemclphr  7034  caucvgprprlemexbt  7035  nntopi  7199  axcaucvglemres  7204  suprzclex  8603  supinfneg  8841  infsupneg  8842  ublbneg  8856  exbtwnzlemstep  9411  exbtwnzlemshrink  9412  rebtwn2zlemstep  9416  rebtwn2zlemshrink  9417  hashunlem  9905  cvg1nlemres  10097  resqrexlemoverl  10133  resqrexlemsqa  10136  resqrexlemex  10137  rexanre  10332  rexico  10333  fimaxre2  10335  odd2np1lem  10504  divalglemeunn  10553  divalglemeuneg  10555  bezoutlemex  10622  bj-nn0sucALT  11065
  Copyright terms: Public domain W3C validator