Theorem cbvral2vw 3249

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

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2840  df-ral 3082

This theorem is used by:  cbvral3vw  3251  cbvral6vw  3253  fununi  6615  fiint  9293  nqereu  10933  mgmhmpropd  18792  mhmpropd  18891  efgred  19866  mplcoe5  22245  mdetunilem9  22831  fbun  24052  fbunfip  24081  caucfil  25497  pmltpc  25664  negsprop  28283  iscgrglt  28838  axcontlem10  29382  htth  31345  cdj3lem3b  32867  cdj3i  32868  dfmgc2  33384  isros  34627  rossros  34639  nadddilem2  36754  nadddilem4  36756  fipjust  44368  isotone1  44851  isotone2  44852  ntrclsiso  44870  ntrclskb  44872  ntrclsk3  44873  ntrclsk13  44874  limsuppnfd  46493  pimincfltioo  47509  incsmf  47533  decsmf  47558  catprslem  49864  isthincd2lem1  50279  isthincd2lem2  50289