![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvalv | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2059. (Revised by Wolf Lammen, 17-Jul-2021.) |
Ref | Expression |
---|---|
cbvalv.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvalv | ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1879 | . . . 4 ⊢ (𝜑 → ∀𝑦𝜑) | |
2 | 1 | hbal 2076 | . . 3 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) |
3 | cbvalv.1 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 3 | spv 2296 | . . 3 ⊢ (∀𝑥𝜑 → 𝜓) |
5 | 2, 4 | alrimih 1791 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) |
6 | ax-5 1879 | . . . 4 ⊢ (𝜓 → ∀𝑥𝜓) | |
7 | 6 | hbal 2076 | . . 3 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) |
8 | 3 | equcoms 1993 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) |
9 | 8 | bicomd 213 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜑)) |
10 | 9 | spv 2296 | . . 3 ⊢ (∀𝑦𝜓 → 𝜑) |
11 | 7, 10 | alrimih 1791 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑) |
12 | 5, 11 | impbii 199 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∀wal 1521 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-11 2074 ax-12 2087 ax-13 2282 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 |
This theorem is referenced by: cbvexv 2311 cbvaldva 2317 cbval2v 2321 nfcjust 2781 cdeqal1 3459 zfpow 4874 tfisi 7100 pssnn 8219 findcard 8240 findcard3 8244 zfinf 8574 aceq0 8979 kmlem1 9010 kmlem13 9022 fin23lem32 9204 fin23lem41 9212 zfac 9320 zfcndpow 9476 zfcndinf 9478 zfcndac 9479 axgroth4 9692 relexpindlem 13847 ramcl 15780 mreexexlemd 16351 bnj1112 31177 dfon2lem6 31817 dfon2lem7 31818 dfon2 31821 phpreu 33523 axc11n-16 34542 dfac11 37949 |
Copyright terms: Public domain | W3C validator |