![]() |
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 3358 with a disjoint variable condition, which does not require ax-13 2372. For a version not dependent on ax-11 2155 and ax-12, see cbvrexvw 3236. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2138, ax-13 2372. (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 1861 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
5 | cbvrexfw.4 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | nfn 1861 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
7 | cbvrexfw.5 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
8 | 7 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
9 | 1, 2, 4, 6, 8 | cbvralfw 3302 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓) |
10 | ralnex 3073 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
11 | ralnex 3073 | . . 3 ⊢ (∀𝑦 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜓) | |
12 | 9, 10, 11 | 3bitr3i 301 | . 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜓) |
13 | 12 | con4bii 321 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 Ⅎwnf 1786 Ⅎwnfc 2884 ∀wral 3062 ∃wrex 3071 |
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 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-nf 1787 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 |
This theorem is referenced by: cbvrexw 3305 reusv2lem4 5400 reusv2 5402 nnwof 12898 cbviunf 31787 ac6sf2 31849 dfimafnf 31860 aciunf1lem 31887 bnj1400 33846 phpreu 36472 poimirlem26 36514 indexa 36601 evth2f 43699 fvelrnbf 43702 evthf 43711 eliin2f 43793 stoweidlem34 44750 ovnlerp 45278 |
Copyright terms: Public domain | W3C validator |