![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvalvw | Structured version Visualization version GIF version |
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2425 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.) |
Ref | Expression |
---|---|
cbvalvw.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvalvw | ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 2009 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) | |
2 | ax-5 2009 | . 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) | |
3 | ax-5 2009 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) | |
4 | ax-5 2009 | . 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) | |
5 | cbvalvw.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvalw 2142 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∀wal 1654 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1879 |
This theorem is referenced by: cbvexvw 2144 hba1w 2149 ax12wdemo 2186 nfcjust 2957 zfpow 5068 tfisi 7324 pssnn 8453 findcard 8474 findcard3 8478 zfinf 8820 aceq0 9261 kmlem1 9294 kmlem13 9306 fin23lem32 9488 fin23lem41 9496 zfac 9604 zfcndpow 9760 zfcndinf 9762 zfcndac 9763 axgroth4 9976 relexpindlem 14187 ramcl 16111 mreexexlemd 16664 bnj1112 31593 dfon2lem6 32226 dfon2lem7 32227 dfon2 32230 bj-ssbjustlem 33153 phpreu 33931 axc11n-16 35008 cbvabvw 38041 dfac11 38470 |
Copyright terms: Public domain | W3C validator |