Theorem cbvral2vw 3385

Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 3388 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 10-Aug-2004.) (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

Step	Hyp	Ref	Expression
1		cbvral2vw.1	. . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))
2	1	ralbidv 3120	. . 3 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	cbvralvw 3372	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)
4		cbvral2vw.2	. . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))
5	4	cbvralvw 3372	. . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑤 ∈ 𝐵 𝜓)
6	5	ralbii 3090	. 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)
7	3, 6	bitri 274	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817  df-ral 3068

This theorem is referenced by:  cbvral3vw  3387  fununi  6493  fiint  9021  nqereu  10616  mhmpropd  18351  efgred  19269  mplcoe5  21151  mdetunilem9  21677  fbun  22899  fbunfip  22928  caucfil  24352  pmltpc  24519  iscgrglt  26779  axcontlem10  27244  htth  29181  cdj3lem3b  30703  cdj3i  30704  dfmgc2  31176  isros  32036  rossros  32048  fipjust  41061  isotone1  41547  isotone2  41548  ntrclsiso  41566  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  limsuppnfd  43133  pimincfltioo  44142  incsmf  44165  decsmf  44189  mgmhmpropd  45227  catprslem  46179  isthincd2lem1  46196  isthincd2lem2  46205