![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvrex2vw | Structured version Visualization version GIF version |
Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 3367 with a disjoint variable condition, which does not require ax-13 2375. (Contributed by FL, 2-Jul-2012.) Avoid ax-13 2375. (Revised by GG, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvrex2vw.1 | ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) |
cbvrex2vw.2 | ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrex2vw | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvrex2vw.1 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) | |
2 | 1 | rexbidv 3177 | . . 3 ⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | cbvrexvw 3236 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
4 | cbvrex2vw.2 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | |
5 | 4 | cbvrexvw 3236 | . . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑤 ∈ 𝐵 𝜓) |
6 | 5 | rexbii 3092 | . 2 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
7 | 3, 6 | bitri 275 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-clel 2814 df-rex 3069 |
This theorem is referenced by: omeu 8622 oeeui 8639 eroveu 8851 genpv 11037 bezoutlem3 16575 bezoutlem4 16576 bezout 16577 4sqlem2 16983 vdwnn 17032 efgrelexlema 19782 dyadmax 25647 2sqlem9 27486 2sq 27489 mulsval2lem 28151 mulsunif2 28211 precsexlemcbv 28245 legov 28608 dfcgra2 28853 gsumwun 33051 pstmfval 33857 satfv0 35343 satfv0fun 35356 fmla1 35372 nn0prpwlem 36305 isbnd2 37770 hashnexinjle 42111 aks6d1c6lem3 42154 nna4b4nsq 42647 oaun3lem1 43364 limsupref 45641 fourierdlem42 46105 fourierdlem54 46116 mogoldbb 47710 |
Copyright terms: Public domain | W3C validator |