Theorem cbvrex2vw 3245

Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 3354 with a disjoint variable condition, which does not require ax-13 2401. (Contributed by FL, 2-Jul-2012.) Avoid ax-13 2401. (Revised by GG, 10-Jan-2024.)

Hypotheses

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

Assertion

Ref	Expression
cbvrex2vw	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)

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

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

Proof of Theorem cbvrex2vw

Step	Hyp	Ref	Expression
1		cbvrex2vw.1	. . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))
2	1	rexbidv 3186	. . 3 ⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	cbvrexvw 3241	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)
4		cbvrex2vw.2	. . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))
5	4	cbvrexvw 3241	. . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑤 ∈ 𝐵 𝜓)
6	5	rexbii 3109	. 2 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)
7	3, 6	bitri 278	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wrex 3086

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 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-rex 3087

This theorem is used by:  omeu  8598  oeeui  8616  eroveu  8838  genpv  11089  bezoutlem3  16721  bezoutlem4  16722  bezout  16723  4sqlem2  17134  vdwnn  17183  efgrelexlema  19970  dyadmax  25926  2sqlem9  27761  2sq  27764  nna4b4nsq  27997  mulsval2lem  28503  mulsunif2  28563  precsexlemcbv  28599  eucliddivs  28769  bdayfinbndcbv  28859  bdayfinbndlem1  28860  bdayfinbndlem2  28861  z12zsodd  28875  legov  29055  dfcgra2  29345  gsumwun  33685  constrcbvlem  34435  pstmfval  34576  satfv0  36211  satfv0fun  36224  fmla1  36240  nn0prpwlem  37204  isbnd2  38824  hashnexinjle  43286  aks6d1c6lem3  43329  oaun3lem1  44483  limsupref  46802  fourierdlem42  47266  fourierdlem54  47277  mogoldbb  48990