Theorem cbvral2v 3362

Description: Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by NM, 10-Aug-2004.)

Hypotheses

Ref	Expression
cbvral2v.1	⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))
cbvral2v.2	⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
cbvral2v	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑧,𝐴   𝑥,𝑦,𝐵   𝑦,𝑧,𝐵   𝑤,𝐵   𝜑,𝑧   𝜓,𝑦   𝜒,𝑥   𝜒,𝑤

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑤)   𝜓(𝑥,𝑧,𝑤)   𝜒(𝑦,𝑧)   𝐴(𝑦,𝑤)

Proof of Theorem cbvral2v

Step	Hyp	Ref	Expression
1		cbvral2v.1	. . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))
2	1	ralbidv 3167	. . 3 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	cbvralv 3354	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)
4		cbvral2v.2	. . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))
5	4	cbvralv 3354	. . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑤 ∈ 𝐵 𝜓)
6	5	ralbii 3161	. 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)
7	3, 6	bitri 267	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 198  ∀wral 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clel 2795  df-nfc 2930  df-ral 3094

This theorem is referenced by:  cbvral3v  3364  fununi  6175  fiint  8479  nqereu  10039  mhmpropd  17656  efgred  18476  mplcoe5  19791  mdetunilem9  20752  fbun  21972  fbunfip  22001  caucfil  23409  pmltpc  23558  iscgrglt  25765  axcontlem10  26210  htth  28300  cdj3lem3b  29824  cdj3i  29825  isros  30747  rossros  30759  fipjust  38653  isotone1  39128  isotone2  39129  ntrclsiso  39147  ntrclskb  39149  ntrclsk3  39150  ntrclsk13  39151  pimincfltioo  41674  incsmf  41697  decsmf  41721  mgmhmpropd  42584