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

Theorem cbvral2vw 3239
Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 3365 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 10-Aug-2004.) Avoid ax-13 2372. (Revised by Gino Giotto, 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 3235 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑦𝐵 𝜒)
4 cbvral2vw.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvralvw 3235 . . 3 (∀𝑦𝐵 𝜒 ↔ ∀𝑤𝐵 𝜓)
65ralbii 3094 . 2 (∀𝑧𝐴𝑦𝐵 𝜒 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 275 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wral 3062
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
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811  df-ral 3063
This theorem is referenced by:  cbvral3vw  3241  cbvral6vw  3243  fununi  6621  fiint  9321  nqereu  10921  mhmpropd  18675  efgred  19611  mplcoe5  21587  mdetunilem9  22114  fbun  23336  fbunfip  23365  caucfil  24792  pmltpc  24959  negsprop  27499  iscgrglt  27755  axcontlem10  28221  htth  30159  cdj3lem3b  31681  cdj3i  31682  dfmgc2  32154  isros  33155  rossros  33167  fipjust  42302  isotone1  42785  isotone2  42786  ntrclsiso  42804  ntrclskb  42806  ntrclsk3  42807  ntrclsk13  42808  limsuppnfd  44405  pimincfltioo  45421  incsmf  45445  decsmf  45470  mgmhmpropd  46542  catprslem  47584  isthincd2lem1  47601  isthincd2lem2  47610
  Copyright terms: Public domain W3C validator