![]() |
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 3365 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 3178 | . . 3 ⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | cbvrexvw 3235 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
4 | cbvrex2vw.2 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | |
5 | 4 | cbvrexvw 3235 | . . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑤 ∈ 𝐵 𝜓) |
6 | 5 | rexbii 3094 | . 2 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
7 | 3, 6 | bitri 274 | 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 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-clel 2810 df-rex 3071 |
This theorem is referenced by: omeu 8587 oeeui 8604 eroveu 8808 genpv 10996 bezoutlem3 16485 bezoutlem4 16486 bezout 16487 4sqlem2 16884 vdwnn 16933 efgrelexlema 19619 dyadmax 25122 2sqlem9 26937 2sq 26940 mulsval2lem 27576 precsexlemcbv 27662 legov 27874 dfcgra2 28119 pstmfval 32945 satfv0 34418 satfv0fun 34431 fmla1 34447 nn0prpwlem 35293 isbnd2 36737 nna4b4nsq 41484 oaun3lem1 42206 limsupref 44480 fourierdlem42 44944 fourierdlem54 44955 mogoldbb 46532 |
Copyright terms: Public domain | W3C validator |