![]() |
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 3341 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by FL, 2-Jul-2012.) Avoid ax-13 2371. (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvrex2vw.1 | ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) |
cbvrex2vw.2 | ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrex2vw | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvrex2vw.1 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) | |
2 | 1 | rexbidv 3172 | . . 3 ⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | cbvrexvw 3225 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
4 | cbvrex2vw.2 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | |
5 | 4 | cbvrexvw 3225 | . . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑤 ∈ 𝐵 𝜓) |
6 | 5 | rexbii 3094 | . 2 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
7 | 3, 6 | bitri 275 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-clel 2811 df-rex 3071 |
This theorem is referenced by: omeu 8533 oeeui 8550 eroveu 8754 genpv 10940 bezoutlem3 16427 bezoutlem4 16428 bezout 16429 4sqlem2 16826 vdwnn 16875 efgrelexlema 19536 dyadmax 24978 2sqlem9 26791 2sq 26794 legov 27569 dfcgra2 27814 pstmfval 32534 satfv0 34009 satfv0fun 34022 fmla1 34038 nn0prpwlem 34840 isbnd2 36288 nna4b4nsq 41041 oaun3lem1 41733 limsupref 44012 fourierdlem42 44476 fourierdlem54 44487 mogoldbb 46063 |
Copyright terms: Public domain | W3C validator |