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

Theorem cbvrexv 2587
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 1464 . 2 𝑦𝜑
2 nfv 1464 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvrex 2583 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wrex 2356
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361
This theorem is referenced by:  cbvrex2v  2595  reu7  2801  reusv3  4258  funcnvuni  5050  fun11iun  5239  fvelimab  5325  fliftfun  5538  grpridd  5800  tfr1onlemaccex  6069  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllemaccex  6082  tfrcldm  6084  frecsuc  6128  nnaordex  6240  fimax2gtri  6571  supmoti  6635  suplub2ti  6643  fodjuomnilemdc  6746  fodjuomnilemres  6750  fodjuomni  6751  cardval3ex  6760  prarloclemlo  7000  prarloclem3  7003  cauappcvgprlemdisj  7157  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgpr  7168  caucvgprlemdisj  7180  caucvgprlemcl  7182  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgpr  7188  caucvgprprlemell  7191  caucvgprprlemelu  7192  caucvgprprlemlol  7204  caucvgprprlemclphr  7211  caucvgprprlemexbt  7212  nntopi  7376  axcaucvglemres  7381  suprzclex  8780  supinfneg  9018  infsupneg  9019  ublbneg  9033  exbtwnzlemstep  9590  exbtwnzlemshrink  9591  rebtwn2zlemstep  9595  rebtwn2zlemshrink  9596  hashunlem  10130  cvg1nlemres  10335  resqrexlemoverl  10371  resqrexlemsqa  10374  resqrexlemex  10375  rexanre  10570  rexico  10571  fimaxre2  10574  isummolem2  10685  isummo  10686  odd2np1lem  10797  divalglemeunn  10846  divalglemeuneg  10848  bezoutlemex  10915  bj-nn0sucALT  11361
  Copyright terms: Public domain W3C validator