Theorem cbvral2vw 3245

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

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

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 2147

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

This theorem is used by:  cbvral3vw  3247  cbvral6vw  3249  fununi  6615  fiint  9318  nqereu  11014  mgmhmpropd  18887  mhmpropd  18987  efgred  19962  mplcoe5  22349  mdetunilem9  22935  fbun  24159  fbunfip  24188  caucfil  25604  pmltpc  25771  negsprop  28421  iscgrglt  28977  axcontlem10  29551  htth  31520  cdj3lem3b  33042  cdj3i  33043  dfmgc2  33557  isros  34801  rossros  34813  nadddilem2  36970  nadddilem4  36972  fipjust  44565  isotone1  45047  isotone2  45048  ntrclsiso  45066  ntrclskb  45068  ntrclsk3  45069  ntrclsk13  45070  limsuppnfd  46711  pimincfltioo  47727  incsmf  47751  decsmf  47776  catprslem  50117  isthincd2lem1  50532  isthincd2lem2  50542