![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvrex2v | Structured version Visualization version GIF version |
Description: Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by FL, 2-Jul-2012.) |
Ref | Expression |
---|---|
cbvrex2v.1 | ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) |
cbvrex2v.2 | ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrex2v | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvrex2v.1 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) | |
2 | 1 | rexbidv 3242 | . . 3 ⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | cbvrexv 3384 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
4 | cbvrex2v.2 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | |
5 | 4 | cbvrexv 3384 | . . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑤 ∈ 𝐵 𝜓) |
6 | 5 | rexbii 3194 | . 2 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
7 | 3, 6 | bitri 267 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∃wrex 3089 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 |
This theorem is referenced by: omeu 8012 oeeui 8029 eroveu 8192 genpv 10219 bezoutlem3 15745 bezoutlem4 15746 bezout 15747 4sqlem2 16141 vdwnn 16190 efgrelexlema 18635 dyadmax 23902 2sqlem9 25705 2sq 25708 legov 26073 dfcgra2 26318 pstmfval 30786 fmla1 32203 nn0prpwlem 33197 isbnd2 34509 fourierdlem42 41871 fourierdlem54 41882 mogoldbb 43324 |
Copyright terms: Public domain | W3C validator |