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

Theorem cbvral2vw 3460
Description: Version of cbvral2v 3463 with a disjoint variable condition, which does not require ax-13 2383. (Contributed 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 3195 . . 3 (𝑥 = 𝑧 → (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜒))
32cbvralvw 3448 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑦𝐵 𝜒)
4 cbvral2vw.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvralvw 3448 . . 3 (∀𝑦𝐵 𝜒 ↔ ∀𝑤𝐵 𝜓)
65ralbii 3163 . 2 (∀𝑧𝐴𝑦𝐵 𝜒 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 277 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wral 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-clel 2891  df-ral 3141
This theorem is referenced by:  cbvral3vw  3462  fununi  6422  fiint  8787  nqereu  10343  mhmpropd  17954  efgred  18866  mplcoe5  20241  mdetunilem9  21221  fbun  22440  fbunfip  22469  caucfil  23878  pmltpc  24043  iscgrglt  26292  axcontlem10  26751  htth  28687  cdj3lem3b  30209  cdj3i  30210  isros  31415  rossros  31427  fipjust  39909  isotone1  40383  isotone2  40384  ntrclsiso  40402  ntrclskb  40404  ntrclsk3  40405  ntrclsk13  40406  limsuppnfd  41967  pimincfltioo  42981  incsmf  43004  decsmf  43028  mgmhmpropd  44037
  Copyright terms: Public domain W3C validator