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

Theorem cbvrexw 3307
Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 3305 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2377. (Revised by GG, 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 2905 . 2 𝑥𝐴
2 nfcv 2905 . 2 𝑦𝐴
3 cbvralw.1 . 2 𝑦𝜑
4 cbvralw.2 . 2 𝑥𝜓
5 cbvralw.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrexfw 3305 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wnf 1783  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071
This theorem is referenced by:  cbvrexsvw  3318  cbvrexsvwOLD  3321  cbvreuw  3410  reu8nf  3877  cbviun  5036  isarep1  6656  isarep1OLD  6657  fvelimad  6976  dffo3f  7126  elabrex  7262  elabrexg  7263  onminex  7822  boxcutc  8981  indexfi  9400  wdom2d  9620  hsmexlem2  10467  fprodle  16032  iundisj  25583  mbfsup  25699  iundisjf  32602  iundisjfi  32798  voliune  34230  volfiniune  34231  bnj1542  34871  cvmcov  35268  poimirlem24  37651  poimirlem26  37653  indexa  37740  mndmolinv  42096  primrootsunit1  42098  primrootsunit  42099  primrootspoweq0  42107  aks6d1c4  42125  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  rhmqusspan  42186  grpods  42195  unitscyglem1  42196  unitscyglem3  42198  unitscyglem4  42199  rexrabdioph  42805  rexfrabdioph  42806  disjrnmpt2  45193  caucvgbf  45500  limsuppnfd  45717  limsuppnf  45726  limsupre2  45740  limsupre3  45748  limsupre3uz  45751  limsupreuz  45752  liminfreuz  45818  stoweidlem31  46046  stoweidlem59  46074  rexsb  47111  cbvrex2  47116  2reu8i  47125
  Copyright terms: Public domain W3C validator