Theorem cbvrex2vw 3220

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

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

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 2811  df-rex 3062

This theorem is referenced by:  omeu  8520  oeeui  8538  eroveu  8759  genpv  10922  bezoutlem3  16510  bezoutlem4  16511  bezout  16512  4sqlem2  16920  vdwnn  16969  efgrelexlema  19724  dyadmax  25565  2sqlem9  27390  2sq  27393  mulsval2lem  28102  mulsunif2  28162  precsexlemcbv  28198  eucliddivs  28368  bdayfinbndcbv  28458  bdayfinbndlem1  28459  bdayfinbndlem2  28460  z12zsodd  28474  legov  28653  dfcgra2  28898  gsumwun  33137  constrcbvlem  33899  pstmfval  34040  satfv0  35540  satfv0fun  35553  fmla1  35569  nn0prpwlem  36504  isbnd2  38104  hashnexinjle  42568  aks6d1c6lem3  42611  nna4b4nsq  43093  oaun3lem1  43802  limsupref  46113  fourierdlem42  46577  fourierdlem54  46588  mogoldbb  48261