![]() |
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 3333 with a disjoint variable condition, which does not require ax-13 2371. For a version not dependent on ax-11 2155 and ax-12, see cbvrexvw 3225. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2138, ax-13 2371. (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 3286 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓) |
10 | ralnex 3072 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
11 | ralnex 3072 | . . 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 3061 ∃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 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 3062 df-rex 3071 |
This theorem is referenced by: cbvrexw 3289 reusv2lem4 5357 reusv2 5359 nnwof 12844 cbviunf 31520 ac6sf2 31585 dfimafnf 31596 aciunf1lem 31624 bnj1400 33504 phpreu 36108 poimirlem26 36150 indexa 36238 evth2f 43308 fvelrnbf 43311 evthf 43320 eliin2f 43402 stoweidlem34 44361 ovnlerp 44889 |
Copyright terms: Public domain | W3C validator |