![]() |
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 2462. Usage of this theorem is discouraged because it depends on ax-13 2379. See cbvaldw 2347 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2379. (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 1915 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | cbvald.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
3 | cbvald.2 | . 2 ⊢ (𝜑 → Ⅎ𝑦𝜓) | |
4 | nfvd 1916 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
5 | cbvald.3 | . 2 ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) | |
6 | 1, 2, 3, 4, 5 | cbv2 2412 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1536 Ⅎwnf 1785 |
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-11 2158 ax-12 2175 ax-13 2379 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 |
This theorem is referenced by: cbvexd 2418 cbvaldva 2419 axextnd 10002 axrepndlem1 10003 axunndlem1 10006 axpowndlem2 10009 axpowndlem3 10010 axpowndlem4 10011 axregndlem2 10014 axregnd 10015 axinfnd 10017 axacndlem5 10022 axacnd 10023 axextdist 33157 distel 33161 wl-sb8eut 34978 |
Copyright terms: Public domain | W3C validator |