Theorem cbvrex2vw 3215

Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 3335 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by FL, 2-Jul-2012.) Avoid ax-13 2372. (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 3156	. . 3 ⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	cbvrexvw 3211	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)
4		cbvrex2vw.2	. . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))
5	4	cbvrexvw 3211	. . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑤 ∈ 𝐵 𝜓)
6	5	rexbii 3079	. 2 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)
7	3, 6	bitri 275	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-rex 3057

This theorem is referenced by:  omeu  8500  oeeui  8517  eroveu  8736  genpv  10890  bezoutlem3  16452  bezoutlem4  16453  bezout  16454  4sqlem2  16861  vdwnn  16910  efgrelexlema  19661  dyadmax  25526  2sqlem9  27365  2sq  27368  mulsval2lem  28049  mulsunif2  28109  precsexlemcbv  28144  eucliddivs  28301  zs12zodd  28392  legov  28563  dfcgra2  28808  gsumwun  33045  constrcbvlem  33768  pstmfval  33909  satfv0  35402  satfv0fun  35415  fmla1  35431  nn0prpwlem  36364  isbnd2  37831  hashnexinjle  42170  aks6d1c6lem3  42213  nna4b4nsq  42701  oaun3lem1  43415  limsupref  45731  fourierdlem42  46195  fourierdlem54  46206  mogoldbb  47824