Theorem cbvral2vw 3238

Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 3364 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 10-Aug-2004.) Avoid ax-13 2371. (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 3177	. . 3 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	cbvralvw 3234	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)
4		cbvral2vw.2	. . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))
5	4	cbvralvw 3234	. . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑤 ∈ 𝐵 𝜓)
6	5	ralbii 3093	. 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)
7	3, 6	bitri 274	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2810  df-ral 3062

This theorem is referenced by:  cbvral3vw  3240  cbvral6vw  3242  fununi  6623  fiint  9326  nqereu  10926  mhmpropd  18680  efgred  19618  mplcoe5  21601  mdetunilem9  22129  fbun  23351  fbunfip  23380  caucfil  24807  pmltpc  24974  negsprop  27519  iscgrglt  27803  axcontlem10  28269  htth  30209  cdj3lem3b  31731  cdj3i  31732  dfmgc2  32204  isros  33235  rossros  33247  fipjust  42398  isotone1  42881  isotone2  42882  ntrclsiso  42900  ntrclskb  42902  ntrclsk3  42903  ntrclsk13  42904  limsuppnfd  44497  pimincfltioo  45513  incsmf  45537  decsmf  45562  mgmhmpropd  46634  catprslem  47708  isthincd2lem1  47725  isthincd2lem2  47734