![]() |
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 2444. Usage of this theorem is discouraged because it depends on ax-13 2365. See cbvaldw 2328 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2365. (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 1909 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | cbvald.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
3 | cbvald.2 | . 2 ⊢ (𝜑 → Ⅎ𝑦𝜓) | |
4 | nfvd 1910 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
5 | cbvald.3 | . 2 ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) | |
6 | 1, 2, 3, 4, 5 | cbv2 2396 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1531 Ⅎwnf 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-11 2146 ax-12 2166 ax-13 2365 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1774 df-nf 1778 |
This theorem is referenced by: cbvexd 2401 cbvaldva 2402 axextnd 10616 axrepndlem1 10617 axunndlem1 10620 axpowndlem2 10623 axpowndlem3 10624 axpowndlem4 10625 axregndlem2 10628 axregnd 10629 axinfnd 10631 axacndlem5 10636 axacnd 10637 axextdist 35523 distel 35527 wl-sb8eut 37173 |
Copyright terms: Public domain | W3C validator |