![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvrexfw | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3386 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by FL, 27-Apr-2008.) (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvrexfw.1 | ⊢ Ⅎ𝑥𝐴 |
cbvrexfw.2 | ⊢ Ⅎ𝑦𝐴 |
cbvrexfw.3 | ⊢ Ⅎ𝑦𝜑 |
cbvrexfw.4 | ⊢ Ⅎ𝑥𝜓 |
cbvrexfw.5 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrexfw | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvrexfw.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
2 | cbvrexfw.2 | . . . 4 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvrexfw.3 | . . . . 5 ⊢ Ⅎ𝑦𝜑 | |
4 | 3 | nfn 1858 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
5 | cbvrexfw.4 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | nfn 1858 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
7 | cbvrexfw.5 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
8 | 7 | notbid 321 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
9 | 1, 2, 4, 6, 8 | cbvralfw 3382 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓) |
10 | 9 | notbii 323 | . 2 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓) |
11 | dfrex2 3202 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
12 | dfrex2 3202 | . 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓) | |
13 | 10, 11, 12 | 3bitr4i 306 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 Ⅎwnf 1785 Ⅎwnfc 2936 ∀wral 3106 ∃wrex 3107 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-11 2158 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 |
This theorem is referenced by: cbvrexw 3388 reusv2lem4 5267 reusv2 5269 nnwof 12302 cbviunf 30319 ac6sf2 30384 dfimafnf 30395 aciunf1lem 30425 bnj1400 32217 phpreu 35041 poimirlem26 35083 indexa 35171 evth2f 41644 fvelrnbf 41647 evthf 41656 eliin2f 41740 stoweidlem34 42676 ovnlerp 43201 |
Copyright terms: Public domain | W3C validator |