| 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 2456. Usage of this theorem is discouraged because it depends on ax-13 2377. See cbvaldw 2340 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2377. (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 1914 | . 2 ⊢ Ⅎ𝑥𝜑 | |
| 2 | cbvald.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
| 3 | cbvald.2 | . 2 ⊢ (𝜑 → Ⅎ𝑦𝜓) | |
| 4 | nfvd 1915 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
| 5 | cbvald.3 | . 2 ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) | |
| 6 | 1, 2, 3, 4, 5 | cbv2 2408 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-11 2157 ax-12 2177 ax-13 2377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: cbvexd 2413 cbvaldva 2414 axextnd 10631 axrepndlem1 10632 axunndlem1 10635 axpowndlem2 10638 axpowndlem3 10639 axpowndlem4 10640 axregndlem2 10643 axregnd 10644 axinfnd 10646 axacndlem5 10651 axacnd 10652 axextdist 35800 distel 35804 wl-sb8eut 37579 |
| Copyright terms: Public domain | W3C validator |