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

Theorem cbvral2vw 3241
Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 3368 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 10-Aug-2004.) Avoid ax-13 2377. (Revised by GG, 10-Jan-2024.)
Hypotheses
Ref Expression
cbvral2vw.1 (𝑥 = 𝑧 → (𝜑𝜒))
cbvral2vw.2 (𝑦 = 𝑤 → (𝜒𝜓))
Assertion
Ref Expression
cbvral2vw (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
Distinct variable groups:   𝑥,𝑧   𝑦,𝑤   𝑥,𝐴,𝑧   𝑥,𝑦,𝐵,𝑧   𝑤,𝐵   𝜑,𝑧   𝜓,𝑦   𝜒,𝑥   𝜒,𝑤
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑤)   𝜓(𝑥,𝑧,𝑤)   𝜒(𝑦,𝑧)   𝐴(𝑦,𝑤)

Proof of Theorem cbvral2vw
StepHypRef Expression
1 cbvral2vw.1 . . . 4 (𝑥 = 𝑧 → (𝜑𝜒))
21ralbidv 3178 . . 3 (𝑥 = 𝑧 → (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜒))
32cbvralvw 3237 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑦𝐵 𝜒)
4 cbvral2vw.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvralvw 3237 . . 3 (∀𝑦𝐵 𝜒 ↔ ∀𝑤𝐵 𝜓)
65ralbii 3093 . 2 (∀𝑧𝐴𝑦𝐵 𝜒 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 275 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wral 3061
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
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816  df-ral 3062
This theorem is referenced by:  cbvral3vw  3243  cbvral6vw  3245  fununi  6641  fiint  9366  fiintOLD  9367  nqereu  10969  mgmhmpropd  18711  mhmpropd  18805  efgred  19766  mplcoe5  22058  mdetunilem9  22626  fbun  23848  fbunfip  23877  caucfil  25317  pmltpc  25485  negsprop  28067  iscgrglt  28522  axcontlem10  28988  htth  30937  cdj3lem3b  32459  cdj3i  32460  dfmgc2  32986  isros  34169  rossros  34181  fipjust  43578  isotone1  44061  isotone2  44062  ntrclsiso  44080  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  limsuppnfd  45717  pimincfltioo  46733  incsmf  46757  decsmf  46782  catprslem  48899  isthincd2lem1  49075  isthincd2lem2  49084
  Copyright terms: Public domain W3C validator