Theorem cbvrex2vw 3386

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

Syntax hints:   → wi 4   ↔ wb 205  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817  df-rex 3069

This theorem is referenced by:  omeu  8378  oeeui  8395  eroveu  8559  genpv  10686  bezoutlem3  16177  bezoutlem4  16178  bezout  16179  4sqlem2  16578  vdwnn  16627  efgrelexlema  19270  dyadmax  24667  2sqlem9  26480  2sq  26483  legov  26850  dfcgra2  27095  pstmfval  31748  satfv0  33220  satfv0fun  33233  fmla1  33249  nn0prpwlem  34438  isbnd2  35868  nna4b4nsq  40413  limsupref  43116  fourierdlem42  43580  fourierdlem54  43591  mogoldbb  45125