Theorem cbvral2vw 3248

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2839  df-ral 3081

This theorem is used by:  cbvral3vw  3250  cbvral6vw  3252  fununi  6626  fiint  9332  nqereu  11027  mgmhmpropd  18902  mhmpropd  19002  efgred  19977  mplcoe5  22364  mdetunilem9  22950  fbun  24174  fbunfip  24203  caucfil  25619  pmltpc  25786  negsprop  28436  iscgrglt  28992  axcontlem10  29566  htth  31535  cdj3lem3b  33057  cdj3i  33058  dfmgc2  33613  isros  34857  rossros  34869  nadddilem2  37100  nadddilem4  37102  fipjust  44709  isotone1  45191  isotone2  45192  ntrclsiso  45210  ntrclskb  45212  ntrclsk3  45213  ntrclsk13  45214  limsuppnfd  46854  pimincfltioo  47870  incsmf  47894  decsmf  47919  catprslem  50266  isthincd2lem1  50702  isthincd2lem2  50712