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

Theorem cbvrexv 2630
Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)
Hypothesis
Ref Expression
cbvralv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrexv (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrexv
StepHypRef Expression
1 nfv 1491 . 2 𝑦𝜑
2 nfv 1491 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvrex 2626 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wrex 2392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rex 2397
This theorem is referenced by:  cbvrex2v  2638  reu7  2850  reusv3  4349  funcnvuni  5160  fun11iun  5354  fvelimab  5443  fliftfun  5663  grpridd  5933  tfr1onlemaccex  6211  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllemaccex  6224  tfrcldm  6226  frecsuc  6270  nnaordex  6389  fimax2gtri  6761  supmoti  6846  suplub2ti  6854  fodjuomnilemdc  6982  fodjuomnilemres  6986  fodjuomni  6987  fodjumkvlemres  6999  fodjumkv  7000  cardval3ex  7007  prarloclemlo  7266  prarloclem3  7269  cauappcvgprlemdisj  7423  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  cauappcvgpr  7434  caucvgprlemdisj  7446  caucvgprlemcl  7448  caucvgprlemladdfu  7449  caucvgprlemladdrl  7450  caucvgpr  7454  caucvgprprlemell  7457  caucvgprprlemelu  7458  caucvgprprlemlol  7470  caucvgprprlemclphr  7477  caucvgprprlemexbt  7478  suplocexprlemmu  7490  suplocexpr  7497  suplocsrlem  7580  nntopi  7666  axcaucvglemres  7671  axpre-suploc  7674  suprzclex  9100  supinfneg  9339  infsupneg  9340  ublbneg  9354  exbtwnzlemstep  9965  exbtwnzlemshrink  9966  rebtwn2zlemstep  9970  rebtwn2zlemshrink  9971  hashunlem  10490  cvg1nlemres  10697  resqrexlemoverl  10733  resqrexlemsqa  10736  resqrexlemex  10737  rexanre  10932  rexico  10933  fimaxre2  10938  summodclem2  11091  summodc  11092  mertenslemub  11243  mertensabs  11246  odd2np1lem  11465  divalglemeunn  11514  divalglemeuneg  11516  bezoutlemex  11585  ennnfoneleminc  11819  ennnfonelemex  11822  ennnfonelemhom  11823  ennnfonelemr  11831  ctinfom  11836  cnptoprest  12303  dedekindeulemuub  12659  dedekindeulemub  12660  dedekindeulemloc  12661  dedekindeulemlub  12662  dedekindeulemlu  12663  bj-nn0sucALT  12978
  Copyright terms: Public domain W3C validator