Theorem cbvrex2vw 3221

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

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

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-rex 3063

This theorem is referenced by:  omeu  8522  oeeui  8540  eroveu  8761  genpv  10922  bezoutlem3  16480  bezoutlem4  16481  bezout  16482  4sqlem2  16889  vdwnn  16938  efgrelexlema  19690  dyadmax  25567  2sqlem9  27406  2sq  27409  mulsval2lem  28118  mulsunif2  28178  precsexlemcbv  28214  eucliddivs  28384  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  z12zsodd  28490  legov  28669  dfcgra2  28914  gsumwun  33170  constrcbvlem  33933  pstmfval  34074  satfv0  35574  satfv0fun  35587  fmla1  35603  nn0prpwlem  36538  isbnd2  38034  hashnexinjle  42499  aks6d1c6lem3  42542  nna4b4nsq  43018  oaun3lem1  43731  limsupref  46043  fourierdlem42  46507  fourierdlem54  46518  mogoldbb  48145