Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cbvald | Structured version Visualization version GIF version |
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2452. Usage of this theorem is discouraged because it depends on ax-13 2373. See cbvaldw 2338 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2373. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
cbvald.1 | ⊢ Ⅎ𝑦𝜑 |
cbvald.2 | ⊢ (𝜑 → Ⅎ𝑦𝜓) |
cbvald.3 | ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) |
Ref | Expression |
---|---|
cbvald | ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1920 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | cbvald.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
3 | cbvald.2 | . 2 ⊢ (𝜑 → Ⅎ𝑦𝜓) | |
4 | nfvd 1921 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
5 | cbvald.3 | . 2 ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) | |
6 | 1, 2, 3, 4, 5 | cbv2 2404 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1539 Ⅎwnf 1789 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-11 2157 ax-12 2174 ax-13 2373 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-ex 1786 df-nf 1790 |
This theorem is referenced by: cbvexd 2409 cbvaldva 2410 axextnd 10331 axrepndlem1 10332 axunndlem1 10335 axpowndlem2 10338 axpowndlem3 10339 axpowndlem4 10340 axregndlem2 10343 axregnd 10344 axinfnd 10346 axacndlem5 10351 axacnd 10352 axextdist 33754 distel 33758 wl-sb8eut 35711 |
Copyright terms: Public domain | W3C validator |