Theorem cbvral2vw 3220

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3052

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 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ral 3053

This theorem is referenced by:  cbvral3vw  3222  cbvral6vw  3224  fununi  6569  fiint  9232  nqereu  10847  mgmhmpropd  18661  mhmpropd  18755  efgred  19718  mplcoe5  22032  mdetunilem9  22599  fbun  23819  fbunfip  23848  caucfil  25264  pmltpc  25431  negsprop  28045  iscgrglt  28600  axcontlem10  29060  htth  31008  cdj3lem3b  32530  cdj3i  32531  dfmgc2  33075  isros  34332  rossros  34344  fipjust  44014  isotone1  44497  isotone2  44498  ntrclsiso  44516  ntrclskb  44518  ntrclsk3  44519  ntrclsk13  44520  limsuppnfd  46152  pimincfltioo  47168  incsmf  47192  decsmf  47217  catprslem  49501  isthincd2lem1  49916  isthincd2lem2  49926