Theorem cbvrex2vw 3222

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

Syntax hints:   → wi 4   ↔ wb 207  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2814  df-rex 3064

This theorem is referenced by:  omeu  8510  oeeui  8528  eroveu  8749  genpv  10913  bezoutlem3  16501  bezoutlem4  16502  bezout  16503  4sqlem2  16911  vdwnn  16960  efgrelexlema  19715  dyadmax  25583  2sqlem9  27408  2sq  27411  mulsval2lem  28120  mulsunif2  28180  precsexlemcbv  28216  eucliddivs  28386  bdayfinbndcbv  28476  bdayfinbndlem1  28477  bdayfinbndlem2  28478  z12zsodd  28492  legov  28671  dfcgra2  28916  gsumwun  33157  constrcbvlem  33939  pstmfval  34080  satfv0  35586  satfv0fun  35599  fmla1  35615  nn0prpwlem  36550  isbnd2  38150  hashnexinjle  42614  aks6d1c6lem3  42657  nna4b4nsq  43110  oaun3lem1  43819  limsupref  46128  fourierdlem42  46592  fourierdlem54  46603  mogoldbb  48276