![]() |
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 2454. Usage of this theorem is discouraged because it depends on ax-13 2375. See cbvaldw 2339 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2375. (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 1912 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | cbvald.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
3 | cbvald.2 | . 2 ⊢ (𝜑 → Ⅎ𝑦𝜓) | |
4 | nfvd 1913 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
5 | cbvald.3 | . 2 ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) | |
6 | 1, 2, 3, 4, 5 | cbv2 2406 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1535 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-11 2155 ax-12 2175 ax-13 2375 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1777 df-nf 1781 |
This theorem is referenced by: cbvexd 2411 cbvaldva 2412 axextnd 10629 axrepndlem1 10630 axunndlem1 10633 axpowndlem2 10636 axpowndlem3 10637 axpowndlem4 10638 axregndlem2 10641 axregnd 10642 axinfnd 10644 axacndlem5 10649 axacnd 10650 axextdist 35781 distel 35785 wl-sb8eut 37559 |
Copyright terms: Public domain | W3C validator |