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

Theorem cbvrexw 3427
 Description: Rule used to change bound variables, using implicit substitution. Version of cbvrex 3432 with a disjoint variable condition, which does not require ax-13 2392. (Contributed by NM, 31-Jul-2003.) (Revised by Gino Giotto, 10-Jan-2024.)
Hypotheses
Ref Expression
cbvralw.1 𝑦𝜑
cbvralw.2 𝑥𝜓
cbvralw.3 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrexw (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Distinct variable group:   𝑥,𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvrexw
StepHypRef Expression
1 nfcv 2982 . 2 𝑥𝐴
2 nfcv 2982 . 2 𝑦𝐴
3 cbvralw.1 . 2 𝑦𝜑
4 cbvralw.2 . 2 𝑥𝜓
5 cbvralw.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrexfw 3423 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1785  ∃wrex 3134 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-11 2162  ax-12 2179 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139 This theorem is referenced by:  cbvrmowOLD  3430  cbvrexsvw  3454  reu8nf  3844  cbviun  4948  isarep1  6431  fvelimad  6721  elabrex  6992  onminex  7513  boxcutc  8497  indexfi  8825  wdom2d  9037  hsmexlem2  9843  fprodle  15348  iundisj  24150  mbfsup  24266  iundisjf  30345  iundisjfi  30525  voliune  31515  volfiniune  31516  bnj1542  32156  cvmcov  32537  poimirlem24  34993  poimirlem26  34995  indexa  35083  rexrabdioph  39591  rexfrabdioph  39592  elabrexg  41535  dffo3f  41669  disjrnmpt2  41680  limsuppnfd  42210  limsuppnf  42219  limsupre2  42233  limsupre3  42241  limsupre3uz  42244  limsupreuz  42245  liminfreuz  42311  stoweidlem31  42539  stoweidlem59  42567  rexsb  43520  cbvrex2  43525  2reu8i  43535
 Copyright terms: Public domain W3C validator