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

Theorem cbvral2vw 3238
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 2374. (Contributed by NM, 10-Aug-2004.) Avoid ax-13 2374. (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 3175 . . 3 (𝑥 = 𝑧 → (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜒))
32cbvralvw 3234 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑦𝐵 𝜒)
4 cbvral2vw.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvralvw 3234 . . 3 (∀𝑦𝐵 𝜒 ↔ ∀𝑤𝐵 𝜓)
65ralbii 3090 . 2 (∀𝑧𝐴𝑦𝐵 𝜒 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 275 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wral 3058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ral 3059
This theorem is referenced by:  cbvral3vw  3240  cbvral6vw  3242  fununi  6642  fiint  9363  fiintOLD  9364  nqereu  10966  mgmhmpropd  18723  mhmpropd  18817  efgred  19780  mplcoe5  22075  mdetunilem9  22641  fbun  23863  fbunfip  23892  caucfil  25330  pmltpc  25498  negsprop  28081  iscgrglt  28536  axcontlem10  29002  htth  30946  cdj3lem3b  32468  cdj3i  32469  dfmgc2  32970  isros  34148  rossros  34160  fipjust  43554  isotone1  44037  isotone2  44038  ntrclsiso  44056  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  limsuppnfd  45657  pimincfltioo  46673  incsmf  46697  decsmf  46722  catprslem  48798  isthincd2lem1  48826  isthincd2lem2  48835
  Copyright terms: Public domain W3C validator