MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvrexv Structured version   Visualization version   GIF version

Theorem cbvrexv 3454
Description: Change the bound variable of a restricted existential quantifier using implicit substitution. See cbvrexvw 3451 based on fewer axioms , but extra disjoint variables. (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 1906 . 2 𝑦𝜑
2 nfv 1906 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvrex 3447 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wrex 3139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2383
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144
This theorem is referenced by:  cbvrex2v  3466  fiunlem  7634  cygablOLD  18942  poimirlem27  34801  poimirlem32  34806  itg2addnclem  34825  rexrabdioph  39271  rexlimdvaacbv  40439  limsupubuzmpt  41880  limsupmnf  41882  limsupre2  41886  limsupmnfuzlem  41887  limsupmnfuz  41888  limsupre2mpt  41891  limsupre3  41894  limsupre3mpt  41895  limsupre3uz  41897  limsupreuz  41898  limsupreuzmpt  41900  supcnvlimsup  41901  climuz  41905  lmbr3  41908  climrescn  41909  limsuplt2  41914  liminflelimsup  41937  limsupgt  41939  liminfreuz  41964  liminflt  41966  xlimpnfxnegmnf  41975  xlimmnf  42002  xlimpnf  42003  xlimmnfmpt  42004  xlimpnfmpt  42005  dfxlim2  42009  cncfshiftioo  42055  itgiccshift  42145  itgperiod  42146  fourierdlem42  42315  fourierdlem48  42320  fourierdlem81  42353  fourierdlem92  42364  fourierdlem96  42368  fourierdlem97  42369  fourierdlem98  42370  fourierdlem99  42371  fourierdlem105  42377  fourierdlem108  42380  fourierdlem110  42382  fourierdlem112  42384  fourierdlem113  42385  meaiuninc3v  42647  hoidmvval0  42750  ovnhoi  42766  ovolval5lem3  42817  ovolval5  42818  smfsup  42969  smfinflem  42972  smfinf  42973  2reuimp0  43194  fmtnofac2lem  43577  smndex1mgm  43977  smndex1mndlem  43979  2zlidl  44103  2zrngamgm  44108  2zrngagrp  44112  2zrngmmgm  44115  eenglngeehlnmlem1  44622
  Copyright terms: Public domain W3C validator