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

Theorem cbvrexw 3289
Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 3287 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2371. (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 2904 . 2 𝑥𝐴
2 nfcv 2904 . 2 𝑦𝐴
3 cbvralw.1 . 2 𝑦𝜑
4 cbvralw.2 . 2 𝑥𝜓
5 cbvralw.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrexfw 3287 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wnf 1786  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-11 2155  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-clel 2811  df-nfc 2886  df-ral 3062  df-rex 3071
This theorem is referenced by:  cbvrexsvw  3300  cbvreuw  3382  cbvrmowOLD  3387  reu8nf  3834  cbviun  4997  isarep1  6591  isarep1OLD  6592  fvelimad  6910  elabrex  7191  onminex  7738  boxcutc  8882  indexfi  9307  wdom2d  9521  hsmexlem2  10368  fprodle  15884  iundisj  24928  mbfsup  25044  iundisjf  31553  iundisjfi  31746  voliune  32885  volfiniune  32886  bnj1542  33526  cvmcov  33914  poimirlem24  36148  poimirlem26  36150  indexa  36238  rexrabdioph  41160  rexfrabdioph  41161  elabrexg  43337  dffo3f  43486  disjrnmpt2  43495  caucvgbf  43811  limsuppnfd  44029  limsuppnf  44038  limsupre2  44052  limsupre3  44060  limsupre3uz  44063  limsupreuz  44064  liminfreuz  44130  stoweidlem31  44358  stoweidlem59  44386  rexsb  45417  cbvrex2  45422  2reu8i  45431
  Copyright terms: Public domain W3C validator